diff --git a/thys/Automatic_Refinement/Lib/Refine_Util.thy b/thys/Automatic_Refinement/Lib/Refine_Util.thy --- a/thys/Automatic_Refinement/Lib/Refine_Util.thy +++ b/thys/Automatic_Refinement/Lib/Refine_Util.thy @@ -1,964 +1,963 @@ section "General Utilities" theory Refine_Util imports Refine_Util_Bootstrap1 Mpat_Antiquot Mk_Term_Antiquot begin definition conv_tag where "conv_tag n x == x" \ \Used internally for @{text "pat_conv"}-conversion\ lemma shift_lambda_left: "(f \ \x. g x) \ (\x. f x \ g x)" by simp ML \ infix 0 THEN_ELSE' THEN_ELSE_COMB' infix 1 THEN_ALL_NEW_FWD THEN_INTERVAL infix 2 ORELSE_INTERVAL infix 3 ->> signature BASIC_REFINE_UTIL = sig include BASIC_REFINE_UTIL (* Resolution with matching *) val RSm: Proof.context -> thm -> thm -> thm val is_Abs: term -> bool val is_Comb: term -> bool val has_Var: term -> bool val is_TFree: typ -> bool val is_def_thm: thm -> bool (* Tacticals *) type tactic' = int -> tactic type itactic = int -> int -> tactic val IF_EXGOAL: (int -> tactic) -> tactic' val COND': (term -> bool) -> tactic' val CONCL_COND': (term -> bool) -> tactic' val THEN_ELSE': tactic' * (tactic' * tactic') -> tactic' val THEN_ELSE_COMB': tactic' * ((tactic'*tactic'->tactic') * tactic' * tactic') -> tactic' val INTERVAL_FWD: tactic' -> int -> int -> tactic val THEN_ALL_NEW_FWD: tactic' * tactic' -> tactic' val REPEAT_ALL_NEW_FWD: tactic' -> tactic' val REPEAT_DETERM': tactic' -> tactic' val REPEAT': tactic' -> tactic' val ALL_GOALS_FWD': tactic' -> tactic' val ALL_GOALS_FWD: tactic' -> tactic val APPEND_LIST': tactic' list -> tactic' val SINGLE_INTERVAL: itactic -> tactic' val THEN_INTERVAL: itactic * itactic -> itactic val ORELSE_INTERVAL: itactic * itactic -> itactic val CAN': tactic' -> tactic' val NTIMES': tactic' -> int -> tactic' (* Only consider results that solve subgoal. If none, return all results unchanged. *) val TRY_SOLVED': tactic' -> tactic' (* Case distinction with tactics. Generalization of THEN_ELSE to lists. *) val CASES': (tactic' * tactic) list -> tactic' (* Tactic that depends on subgoal term structure *) val WITH_subgoal: (term -> tactic') -> tactic' (* Tactic that depends on subgoal's conclusion term structure *) val WITH_concl: (term -> tactic') -> tactic' (* Tactic version of Variable.trade. Import, apply tactic, and export results. One effect is that schematic variables in the goal are fixed, and thus cannot be instantiated by the tactic. *) val TRADE: (Proof.context -> tactic') -> Proof.context -> tactic' (* Tactics *) val fo_rtac: thm -> Proof.context -> tactic' val fo_resolve_tac: thm list -> Proof.context -> tactic' val rprems_tac: Proof.context -> tactic' val rprem_tac: int -> Proof.context -> tactic' val elim_all_tac: Proof.context -> thm list -> tactic val prefer_tac: int -> tactic val insert_subgoal_tac: cterm -> tactic' val insert_subgoals_tac: cterm list -> tactic' val eqsubst_inst_tac: Proof.context -> bool -> int list -> ((indexname * Position.T) * string) list -> thm -> int -> tactic val eqsubst_inst_meth: (Proof.context -> Proof.method) context_parser (* Parsing *) val ->> : 'a context_parser *('a * Context.generic -> 'b * Context.generic) -> 'b context_parser end signature REFINE_UTIL = sig include BASIC_REFINE_UTIL val order_by: ('a * 'a -> order) -> ('b -> 'a) -> 'b list -> 'b list val build_res_net: thm list -> (int * thm) Net.net (* Terms *) val fo_matchp: theory -> cterm -> term -> term list option val fo_matches: theory -> cterm -> term -> bool val anorm_typ: typ -> typ val anorm_term: term -> term val import_cterms: bool -> cterm list -> Proof.context -> cterm list * Proof.context val subsume_sort: ('a -> term) -> theory -> 'a list -> 'a list val subsume_sort_gen: ('a -> term) -> Context.generic -> 'a list -> 'a list val mk_compN1: typ list -> int -> term -> term -> term val mk_compN: int -> term -> term -> term val dest_itselfT: typ -> typ val dummify_tvars: term -> term (* a\\x. f x \ a ?x \ f ?x *) val shift_lambda_left: thm -> thm val shift_lambda_leftN: int -> thm -> thm (* Left-Bracketed Structures *) (* Map [] to z, and [x1,...,xN] to f(...f(f(x1,x2),x3)...) *) val list_binop_left: 'a -> ('a * 'a -> 'a) -> 'a list -> 'a (* Map [] to z, [x] to i x, [x1,...,xN] to f(...f(f(x1,x2),x3)...), thread state *) val fold_binop_left: ('c -> 'b * 'c) -> ('a -> 'c -> 'b * 'c) -> ('b * 'b -> 'b) -> 'a list -> 'c -> 'b * 'c (* Tuples, handling () as empty tuple *) val strip_prodT_left: typ -> typ list val list_prodT_left: typ list -> typ val mk_ltuple: term list -> term (* Fix a tuple of new frees *) val fix_left_tuple_from_Ts: string -> typ list -> Proof.context -> term * Proof.context (* HO-Patterns with tuples *) (* Lambda-abstraction over list of terms, recognizing tuples *) val lambda_tuple: term list -> term -> term (* Instantiate tuple-types in specified variables *) val instantiate_tuples: Proof.context -> (indexname*typ) list -> thm -> thm (* Instantiate tuple-types in variables from given term *) val instantiate_tuples_from_term_tac: Proof.context -> term -> tactic (* Instantiate tuple types in variables of subgoal *) val instantiate_tuples_subgoal_tac: Proof.context -> tactic' (* Rules *) val abs_def: Proof.context -> thm -> thm (* Rule combinators *) (* Iterate rule on theorem until it fails *) val repeat_rule: (thm -> thm) -> thm -> thm (* Apply rule on theorem and assert that theorem was changed *) val changed_rule: (thm -> thm) -> thm -> thm (* Try rule on theorem, return theorem unchanged if rule fails *) val try_rule: (thm -> thm) -> thm -> thm (* Singleton version of Variable.trade *) val trade_rule: (Proof.context -> thm -> thm) -> Proof.context -> thm -> thm (* Combine with first matching theorem *) val RS_fst: thm -> thm list -> thm (* Instantiate first matching theorem *) val OF_fst: thm list -> thm list -> thm (* Conversion *) val trace_conv: conv val monitor_conv: string -> conv -> conv val monitor_conv': string -> (Proof.context -> conv) -> Proof.context -> conv val fixup_vars: cterm -> thm -> thm val fixup_vars_conv: conv -> conv val fixup_vars_conv': (Proof.context -> conv) -> Proof.context -> conv val pat_conv': cterm -> (string -> Proof.context -> conv) -> Proof.context -> conv val pat_conv: cterm -> (Proof.context -> conv) -> Proof.context -> conv val HOL_concl_conv: (Proof.context -> conv) -> Proof.context -> conv val import_conv: (Proof.context -> conv) -> Proof.context -> conv val fix_conv: Proof.context -> conv -> conv val ite_conv: conv -> conv -> conv -> conv val cfg_trace_f_tac_conv: bool Config.T val f_tac_conv: Proof.context -> (term -> term) -> (Proof.context -> tactic) -> conv (* Conversion combinators to choose first matching position *) (* Try argument, then function *) val fcomb_conv: conv -> conv (* Descend over function or abstraction *) val fsub_conv: (Proof.context -> conv) -> Proof.context -> conv (* Apply to topmost matching position *) val ftop_conv: (Proof.context -> conv) -> Proof.context -> conv (* Parsing *) val parse_bool_config: string -> bool Config.T -> bool context_parser val parse_paren_list: 'a context_parser -> 'a list context_parser val parse_paren_lists: 'a context_parser -> 'a list list context_parser (* 2-step configuration parser *) (* Parse boolean config, name or no_name. *) val parse_bool_config': string -> bool Config.T -> Token.T list -> (bool Config.T * bool) * Token.T list (* Parse optional (p1,...,pn). Empty list if nothing parsed. *) val parse_paren_list': 'a parser -> Token.T list -> 'a list * Token.T list (* Apply list of (config,value) pairs *) val apply_configs: ('a Config.T * 'a) list -> Proof.context -> Proof.context end structure Refine_Util: REFINE_UTIL = struct open Basic_Refine_Util fun RSm ctxt thA thB = let val (thA, ctxt') = ctxt |> Variable.declare_thm thA |> Variable.declare_thm thB |> yield_singleton (apfst snd oo Variable.import true) thA val thm = thA RS thB val thm = singleton (Variable.export ctxt' ctxt) thm |> Drule.zero_var_indexes in thm end fun is_Abs (Abs _) = true | is_Abs _ = false fun is_Comb (_$_) = true | is_Comb _ = false fun has_Var (Var _) = true | has_Var (Abs (_,_,t)) = has_Var t | has_Var (t1$t2) = has_Var t1 orelse has_Var t2 | has_Var _ = false fun is_TFree (TFree _) = true | is_TFree _ = false fun is_def_thm thm = case thm |> Thm.prop_of of Const (@{const_name "Pure.eq"},_)$_$_ => true | _ => false type tactic' = int -> tactic type itactic = int -> int -> tactic (* Fail if subgoal does not exist *) fun IF_EXGOAL tac i st = if i <= Thm.nprems_of st then tac i st else no_tac st; fun COND' P = IF_EXGOAL (fn i => fn st => (if P (Thm.prop_of st |> curry Logic.nth_prem i) then all_tac st else no_tac st) handle TERM _ => no_tac st | Pattern.MATCH => no_tac st ) (* FIXME: Subtle difference between Logic.concl_of_goal and this: concl_of_goal converts loose bounds to frees! *) fun CONCL_COND' P = COND' (strip_all_body #> Logic.strip_imp_concl #> P) fun (tac1 THEN_ELSE' (tac2,tac3)) x = tac1 x THEN_ELSE (tac2 x,tac3 x); (* If first tactic succeeds, combine its effect with "comb tac2", otherwise use tac_else. Example: tac1 THEN_ELSE_COMB ((THEN_ALL_NEW),tac2,tac_else) *) fun (tac1 THEN_ELSE_COMB' (comb,tac2,tac_else)) i st = let val rseq = tac1 i st in case seq_is_empty rseq of (true,_) => tac_else i st | (false,rseq) => comb (K(K( rseq )), tac2) i st end (* Apply tactic to subgoals in interval, in a forward manner, skipping over emerging subgoals *) fun INTERVAL_FWD tac l u st = if l>u then all_tac st else (tac l THEN (fn st' => let val ofs = Thm.nprems_of st' - Thm.nprems_of st; in if ofs < ~1 then raise THM ( "INTERVAL_FWD: Tac solved more than one goal",~1,[st,st']) else INTERVAL_FWD tac (l+1+ofs) (u+ofs) st' end)) st; (* Apply tac2 to all subgoals emerged from tac1, in forward manner. *) fun (tac1 THEN_ALL_NEW_FWD tac2) i st = (tac1 i THEN (fn st' => INTERVAL_FWD tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) st') ) st; fun REPEAT_ALL_NEW_FWD tac = tac THEN_ALL_NEW_FWD (TRY o (fn i => REPEAT_ALL_NEW_FWD tac i)); (* Repeat tac on subgoal. Determinize each step. Stop if tac fails or subgoal is solved. *) fun REPEAT_DETERM' tac i st = let val n = Thm.nprems_of st in REPEAT_DETERM (COND (has_fewer_prems n) no_tac (tac i)) st end fun REPEAT' tac i st = let val n = Thm.nprems_of st in REPEAT (COND (has_fewer_prems n) no_tac (tac i)) st end (* Apply tactic to all goals in a forward manner. Newly generated goals are ignored. *) fun ALL_GOALS_FWD' tac i st = (tac i THEN (fn st' => let val i' = i + Thm.nprems_of st' + 1 - Thm.nprems_of st; in if i' <= Thm.nprems_of st' then ALL_GOALS_FWD' tac i' st' else all_tac st' end )) st; fun ALL_GOALS_FWD tac = ALL_GOALS_FWD' tac 1; fun APPEND_LIST' tacs = fold_rev (curry (op APPEND')) tacs (K no_tac); fun SINGLE_INTERVAL tac i = tac i i fun ((tac1:itactic) THEN_INTERVAL (tac2:itactic)) = (fn i => fn j => fn st => ( tac1 i j THEN (fn st' => tac2 i (j + Thm.nprems_of st' - Thm.nprems_of st) st') ) st ):itactic fun tac1 ORELSE_INTERVAL tac2 = (fn i => fn j => tac1 i j ORELSE tac2 i j) (* Fail if tac fails, otherwise do nothing *) fun CAN' tac i st = case tac i st |> Seq.pull of NONE => Seq.empty | SOME _ => Seq.single st (* Repeat tactic n times *) fun NTIMES' _ 0 _ st = Seq.single st | NTIMES' tac n i st = (tac THEN' NTIMES' tac (n-1)) i st (* Resolve with rule. Use first-order unification. From cookbook, added exception handling *) fun fo_rtac thm = Subgoal.FOCUS (fn {context = ctxt, concl, ...} => let val concl_pat = Drule.strip_imp_concl (Thm.cprop_of thm) val insts = Thm.first_order_match (concl_pat, concl) in resolve_tac ctxt [Drule.instantiate_normalize insts thm] 1 end handle Pattern.MATCH => no_tac ) fun fo_resolve_tac thms ctxt = FIRST' (map (fn thm => fo_rtac thm ctxt) thms); (* Resolve with premises. Copied and adjusted from Goal.assume_rule_tac. *) fun rprems_tac ctxt = Goal.norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) => let fun non_atomic (Const (@{const_name Pure.imp}, _) $ _ $ _) = true | non_atomic (Const (@{const_name Pure.all}, _) $ _) = true | non_atomic _ = false; val ((_, goal'), ctxt') = Variable.focus_cterm NONE goal ctxt; val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); val ethms = Rs |> map (fn R => (Simplifier.norm_hhf ctxt (Thm.trivial R))); in eresolve_tac ctxt ethms i end ); (* Resolve with premise. Copied and adjusted from Goal.assume_rule_tac. *) fun rprem_tac n ctxt = Goal.norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) => let val ((_, goal'), ctxt') = Variable.focus_cterm NONE goal ctxt; val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; val R = nth (Drule.strip_imp_prems goal'') (n - 1) val rl = Simplifier.norm_hhf ctxt (Thm.trivial R) in eresolve_tac ctxt [rl] i end ); fun elim_all_tac ctxt thms = ALLGOALS (REPEAT_ALL_NEW (ematch_tac ctxt thms)) fun prefer_tac i = defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1) fun order_by ord f = sort (ord o apply2 f) (* CLONE from tactic.ML *) local (*insert one tagged rl into the net*) fun insert_krl (krl as (_,th)) = Net.insert_term (K false) (Thm.concl_of th, krl); in (*build a net of rules for resolution*) fun build_res_net rls = fold_rev insert_krl (tag_list 1 rls) Net.empty; end fun insert_subgoals_tac cts i = PRIMITIVE ( Thm.permute_prems 0 (i - 1) #> fold_rev Thm.implies_intr cts #> Thm.permute_prems 0 (~i + 1) ) fun insert_subgoal_tac ct i = insert_subgoals_tac [ct] i local (* Substitution with dynamic instantiation of parameters. By Lars Noschinski. *) fun eqsubst_tac' ctxt asm = if asm then EqSubst.eqsubst_asm_tac ctxt else EqSubst.eqsubst_tac ctxt fun subst_method inst_tac tac = Args.goal_spec -- Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) -- Scan.optional (Scan.lift (Parse.and_list1 (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Parse.embedded_inner_syntax)) --| Args.$$$ "in")) [] -- Attrib.thms >> (fn (((quant, (asm, occL)), insts), thms) => fn ctxt => METHOD (fn facts => if null insts then quant (Method.insert_tac ctxt facts THEN' tac ctxt asm occL thms) else (case thms of [thm] => quant ( Method.insert_tac ctxt facts THEN' inst_tac ctxt asm occL insts thm) | _ => error "Cannot have instantiations with multiple rules"))); in fun eqsubst_inst_tac ctxt asm occL insts thm = Subgoal.FOCUS ( fn {context=ctxt,...} => let val ctxt' = ctxt |> Proof_Context.set_mode Proof_Context.mode_schematic (* FIXME !? *) val thm' = thm |> Rule_Insts.read_instantiate ctxt' insts [] in eqsubst_tac' ctxt asm occL [thm'] 1 end ) ctxt val eqsubst_inst_meth = subst_method eqsubst_inst_tac eqsubst_tac' end (* Match pattern against term, and return list of values for non-dummy variables. A variable is considered dummy if its name starts with an underscore (_)*) fun fo_matchp thy cpat t = let fun ignore (Var ((name,_),_)) = String.isPrefix "_" name | ignore _ = true; val pat = Thm.term_of cpat; val pvars = fold_aterms ( fn t => fn l => if is_Var t andalso not (ignore t) then t::l else l ) pat [] |> rev val inst = Pattern.first_order_match thy (pat,t) (Vartab.empty,Vartab.empty); in SOME (map (Envir.subst_term inst) pvars) end handle Pattern.MATCH => NONE; val fo_matches = is_some ooo fo_matchp fun anorm_typ ty = let val instT = Term.add_tvarsT ty [] |> map_index (fn (i,(n,s)) => (n,TVar (("t"^string_of_int i,0),s))) val ty = Term.typ_subst_TVars instT ty; in ty end; fun anorm_term t = let val instT = Term.add_tvars t [] |> map_index (fn (i,(n,s)) => (n,TVar (("t"^string_of_int i,0),s))) val t = Term.subst_TVars instT t; val inst = Term.add_vars t [] |> map_index (fn (i,(n,s)) => (n,Var (("v"^string_of_int i,0),s))) val t = Term.subst_Vars inst t; in t end; fun import_cterms is_open cts ctxt = let val ts = map Thm.term_of cts val (ts', ctxt') = Variable.import_terms is_open ts ctxt val cts' = map (Thm.cterm_of ctxt) ts' in (cts', ctxt') end (* Order a list of items such that more specific items come before less specific ones. The term to be compared is extracted by a function that is given as parameter. *) fun subsume_sort f thy items = let val rhss = map (Envir.beta_eta_contract o f) items fun freqf thy net rhs = Net.match_term net rhs |> filter (fn p => Pattern.matches thy (p,rhs)) |> length val net = fold (fn rhs => Net.insert_term_safe (op =) (rhs,rhs)) rhss Net.empty val freqs = map (freqf thy net) rhss val res = freqs ~~ items |> sort (rev_order o int_ord o apply2 fst) |> map snd in res end fun subsume_sort_gen f = subsume_sort f o Context.theory_of fun mk_comp1 env (f, g) = let val fT = fastype_of1 (env, f); val gT = fastype_of1 (env, g); val compT = fT --> gT --> domain_type gT --> range_type fT; in Const ("Fun.comp", compT) $ f $ g end; fun mk_compN1 _ 0 f g = f$g | mk_compN1 env 1 f g = mk_comp1 env (f, g) | mk_compN1 env n f g = let val T = fastype_of1 (env, g) |> domain_type val g = incr_boundvars 1 g $ Bound 0 val env = T::env in Abs ("x"^string_of_int n,T,mk_compN1 env (n-1) f g) end val mk_compN = mk_compN1 [] fun abs_def ctxt = Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def fun trace_conv ct = (tracing (@{make_string} ct); Conv.all_conv ct); fun monitor_conv msg conv ct = let val _ = tracing (msg ^ " (gets): " ^ @{make_string} ct); - val res = conv ct - handle exc => - (if Exn.is_interrupt exc then Exn.reraise exc - else tracing (msg ^ " (raises): " ^ @{make_string} exc); - Exn.reraise exc) + val res = \<^try>\conv ct + catch exc => + (tracing (msg ^ " (raises): " ^ @{make_string} exc); + Exn.reraise exc)\ val _ = tracing (msg ^ " (yields): " ^ @{make_string} res); in res end fun monitor_conv' msg conv ctxt ct = monitor_conv msg (conv ctxt) ct fun fixup_vars ct thm = let val lhs = Thm.lhs_of thm val inst = Thm.first_order_match (lhs,ct) val thm' = Thm.instantiate inst thm in thm' end fun fixup_vars_conv conv ct = fixup_vars ct (conv ct) fun fixup_vars_conv' conv ctxt = fixup_vars_conv (conv ctxt) local fun tag_ct ctxt name ct = let val t = Thm.term_of ct; val ty = fastype_of t; val t' = Const (@{const_name conv_tag},@{typ unit}-->ty-->ty) $Free (name,@{typ unit})$t; val ct' = Thm.cterm_of ctxt t'; in ct' end fun mpat_conv pat ctxt ct = let val (tym,tm) = Thm.first_order_match (pat,ct); val tm' = Vars.map (fn ((name, _), _) => tag_ct ctxt name) tm; val ct' = Thm.instantiate_cterm (tym, tm') pat; val goal = Logic.mk_equals (apply2 Thm.term_of (ct, ct')) val goal_ctxt = Variable.declare_term goal ctxt val rthm = Goal.prove_internal goal_ctxt [] (Thm.cterm_of ctxt goal) (K (simp_tac (put_simpset HOL_basic_ss goal_ctxt addsimps @{thms conv_tag_def}) 1)) |> Goal.norm_result ctxt in fixup_vars ct rthm end handle Pattern.MATCH => raise (CTERM ("mpat_conv: No match",[pat,ct])); fun tag_conv cnv ctxt ct = case Thm.term_of ct of Const (@{const_name conv_tag},_)$Free(name,_)$_ => ( (Conv.rewr_conv (@{thm conv_tag_def}) then_conv (cnv name) ctxt) ct) | _ => Conv.all_conv ct; fun all_tag_conv cnv = Conv.bottom_conv (tag_conv cnv); in (* Match against pattern, and apply parameter conversion to matches of variables prefixed by hole_prefix. *) fun pat_conv' cpat cnv ctxt = mpat_conv cpat ctxt then_conv (all_tag_conv cnv ctxt); fun pat_conv cpat conv = pat_conv' cpat (fn name => case name of "HOLE" => conv | _ => K Conv.all_conv); end fun HOL_concl_conv cnv = Conv.params_conv ~1 (fn ctxt => Conv.concl_conv ~1 ( HOLogic.Trueprop_conv (cnv ctxt))); fun import_conv conv ctxt ct = let val (ct',ctxt') = yield_singleton (import_cterms true) ct ctxt val res = conv ctxt' ct' val res' = singleton (Variable.export ctxt' ctxt) res |> fixup_vars ct in res' end fun fix_conv ctxt conv ct = let val thm = conv ct val eq = Logic.mk_equals (Thm.term_of ct, Thm.term_of ct) |> head_of in if (Thm.term_of (Thm.lhs_of thm) aconv Thm.term_of ct) then thm else thm RS Thm.trivial (Thm.mk_binop (Thm.cterm_of ctxt eq) ct (Thm.rhs_of thm)) end fun ite_conv cv cv1 cv2 ct = let val eq1 = SOME (cv ct) handle THM _ => NONE | CTERM _ => NONE | TERM _ => NONE | TYPE _ => NONE; val res = case eq1 of NONE => cv2 ct | SOME eq1 => let val eq2 = cv1 (Thm.rhs_of eq1) in if Thm.is_reflexive eq1 then eq2 else if Thm.is_reflexive eq2 then eq1 else Thm.transitive eq1 eq2 end in res end val cfg_trace_f_tac_conv = Attrib.setup_config_bool @{binding trace_f_tac_conv} (K false) (* Transform term and prove equality to original by tactic *) fun f_tac_conv ctxt f tac ct = let val t = Thm.term_of ct val t' = f t val goal = Logic.mk_equals (t,t') val _ = if Config.get ctxt cfg_trace_f_tac_conv then tracing (Syntax.string_of_term ctxt goal) else () val goal_ctxt = Variable.declare_term goal ctxt val thm = Goal.prove_internal ctxt [] (Thm.cterm_of ctxt goal) (K (tac goal_ctxt)) in thm end (* Apply function to result and context *) fun (p->>f) ctks = let val (res,(context,tks)) = p ctks val (res,context) = f (res, context) in (res,(context,tks)) end fun parse_bool_config name cfg = ( Scan.lift (Args.$$$ name) ->> (apsnd (Config.put_generic cfg true) #>> K true) || Scan.lift (Args.$$$ ("no_"^name)) ->> (apsnd (Config.put_generic cfg false) #>> K false) ) fun parse_paren_list p = Scan.lift ( Args.$$$ "(") |-- Parse.enum1' "," p --| Scan.lift (Args.$$$ ")" ) fun parse_paren_lists p = Scan.repeat (parse_paren_list p) val _ = Theory.setup (Method.setup @{binding fo_rule} (Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' ( fo_resolve_tac thms ctxt))) "resolve using first-order matching" #> Method.setup @{binding rprems} (Scan.lift (Scan.option Parse.nat) >> (fn i => fn ctxt => SIMPLE_METHOD' ( case i of NONE => rprems_tac ctxt | SOME i => rprem_tac i ctxt )) ) "resolve with premises" #> Method.setup @{binding elim_all} (Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (elim_all_tac ctxt thms))) "repeteadly apply elimination rules to all subgoals" #> Method.setup @{binding subst_tac} eqsubst_inst_meth "single-step substitution (dynamic instantiation)" #> Method.setup @{binding clarsimp_all} ( Method.sections Clasimp.clasimp_modifiers >> K (fn ctxt => SIMPLE_METHOD ( CHANGED_PROP (ALLGOALS (Clasimp.clarsimp_tac ctxt)))) ) "simplify and clarify all subgoals") (* Filter alternatives that solve a subgoal. If no alternative solves goal, return result sequence unchanged *) fun TRY_SOLVED' tac i st = let val res = tac i st val solved = Seq.filter (fn st' => Thm.nprems_of st' < Thm.nprems_of st) res in case Seq.pull solved of SOME _ => solved | NONE => res end local fun CASES_aux [] = no_tac | CASES_aux ((tac1, tac2)::cs) = tac1 1 THEN_ELSE (tac2, CASES_aux cs) in (* Accepts a list of pairs of (pattern_tac', worker_tac), and applies worker_tac to results of first successful pattern_tac'. *) val CASES' = SELECT_GOAL o CASES_aux end (* TODO/FIXME: There seem to be no guarantees when eta-long forms are introduced by unification. So, we have to expect eta-long forms everywhere, which may be a problem when matching terms syntactically. *) fun WITH_subgoal tac = CONVERSION Thm.eta_conversion THEN' IF_EXGOAL (fn i => fn st => tac (nth (Thm.prems_of st) (i - 1)) i st) fun WITH_concl tac = CONVERSION Thm.eta_conversion THEN' IF_EXGOAL (fn i => fn st => tac (Logic.concl_of_goal (Thm.prop_of st) i) i st ) fun TRADE tac ctxt i st = let val orig_ctxt = ctxt val (st,ctxt) = yield_singleton (apfst snd oo Variable.import true) st ctxt val seq = tac ctxt i st |> Seq.map (singleton (Variable.export ctxt orig_ctxt)) in seq end (* Try argument, then function *) fun fcomb_conv conv = let open Conv in arg_conv conv else_conv fun_conv conv end (* Descend over function or abstraction *) fun fsub_conv conv ctxt = let open Conv in fcomb_conv (conv ctxt) else_conv abs_conv (conv o snd) ctxt else_conv no_conv end (* Apply to topmost matching position *) fun ftop_conv conv ctxt ct = (conv ctxt else_conv fsub_conv (ftop_conv conv) ctxt) ct (* Iterate rule on theorem until it fails *) fun repeat_rule n thm = case try n thm of SOME thm => repeat_rule n thm | NONE => thm (* Apply rule on theorem and assert that theorem was changed *) fun changed_rule n thm = let val thm' = n thm in if Thm.eq_thm_prop (thm, thm') then raise THM ("Same",~1,[thm,thm']) else thm' end (* Try rule on theorem *) fun try_rule n thm = case try n thm of SOME thm => thm | NONE => thm fun trade_rule f ctxt thm = singleton (Variable.trade (map o f) ctxt) thm fun RS_fst thm thms = let fun r [] = raise THM ("RS_fst, no matches",~1,thm::thms) | r (thm'::thms) = case try (op RS) (thm,thm') of NONE => r thms | SOME thm => thm in r thms end fun OF_fst thms insts = let fun r [] = raise THM ("OF_fst, no matches",length thms,thms@insts) | r (thm::thms) = case try (op OF) (thm,insts) of NONE => r thms | SOME thm => thm in r thms end (* Map [] to z, and [x1,...,xN] to f(...f(f(x1,x2),x3)...) *) fun list_binop_left z f = let fun r [] = z | r [T] = T | r (T::Ts) = f (r Ts,T) in fn l => r (rev l) end (* Map [] to z, [x] to i x, [x1,...,xN] to f(...f(f(x1,x2),x3)...), thread state *) fun fold_binop_left z i f = let fun r [] ctxt = z ctxt | r [T] ctxt = i T ctxt | r (T::Ts) ctxt = let val (Ti,ctxt) = i T ctxt val (Tsi,ctxt) = r Ts ctxt in (f (Tsi,Ti),ctxt) end in fn l => fn ctxt => r (rev l) ctxt end fun strip_prodT_left (Type (@{type_name Product_Type.prod},[A,B])) = strip_prodT_left A @ [B] | strip_prodT_left (Type (@{type_name Product_Type.unit},[])) = [] | strip_prodT_left T = [T] val list_prodT_left = list_binop_left HOLogic.unitT HOLogic.mk_prodT (* Make tuple with left-bracket structure *) val mk_ltuple = list_binop_left HOLogic.unit HOLogic.mk_prod (* Fix a tuple of new frees *) fun fix_left_tuple_from_Ts name = fold_binop_left (fn ctxt => (@{term "()"},ctxt)) (fn T => fn ctxt => let val (x,ctxt) = yield_singleton Variable.variant_fixes name ctxt val x = Free (x,T) in (x,ctxt) end) HOLogic.mk_prod (* Replace all type-vars by dummyT *) val dummify_tvars = map_types (map_type_tvar (K dummyT)) fun dest_itselfT (Type (@{type_name itself},[A])) = A | dest_itselfT T = raise TYPE("dest_itselfT",[T],[]) fun shift_lambda_left thm = thm RS @{thm shift_lambda_left} fun shift_lambda_leftN i = funpow i shift_lambda_left (* TODO: Naming should be without ' for basic parse, and with ' for context_parser! *) fun parse_bool_config' name cfg = (Args.$$$ name #>> K (cfg,true)) || (Args.$$$ ("no_"^name) #>> K (cfg,false)) fun parse_paren_list' p = Scan.optional (Args.parens (Parse.enum1 "," p)) [] fun apply_configs l ctxt = fold (fn (cfg,v) => fn ctxt => Config.put cfg v ctxt) l ctxt fun lambda_tuple [] t = t | lambda_tuple (@{mpat "(?a,?b)"}::l) t = let val body = lambda_tuple (a::b::l) t in @{mk_term "case_prod ?body"} end | lambda_tuple (x::l) t = lambda x (lambda_tuple l t) fun get_tuple_inst ctxt (iname,T) = let val (argTs,T) = strip_type T fun cr (Type (@{type_name prod},[T1,T2])) ctxt = let val (x1,ctxt) = cr T1 ctxt val (x2,ctxt) = cr T2 ctxt in (HOLogic.mk_prod (x1,x2), ctxt) end | cr T ctxt = let val (name, ctxt) = yield_singleton Variable.variant_fixes "x" ctxt in (Free (name,T),ctxt) end val ctxt = Variable.set_body false ctxt (* Prevent generation of skolem-names *) val (args,ctxt) = fold_map cr argTs ctxt fun fl (@{mpat "(?x,?y)"}) = fl x @ fl y | fl t = [t] val fargs = flat (map fl args) val fTs = map fastype_of fargs val v = Var (iname,fTs ---> T) val v = list_comb (v,fargs) val v = lambda_tuple args v in Thm.cterm_of ctxt v end fun instantiate_tuples ctxt inTs = let val inst = inTs ~~ map (get_tuple_inst ctxt) inTs in Thm.instantiate (TVars.empty, Vars.make inst) end val _ = COND' fun instantiate_tuples_from_term_tac ctxt t st = let val vars = Term.add_vars t [] in PRIMITIVE (instantiate_tuples ctxt vars) st end fun instantiate_tuples_subgoal_tac ctxt = WITH_subgoal (fn t => K (instantiate_tuples_from_term_tac ctxt t)) end structure Basic_Refine_Util: BASIC_REFINE_UTIL = Refine_Util open Basic_Refine_Util \ attribute_setup zero_var_indexes = \ Scan.succeed (Thm.rule_attribute [] (K Drule.zero_var_indexes)) \ "Set variable indexes to zero, renaming to avoid clashes" end diff --git a/thys/Automatic_Refinement/Parametricity/Relators.thy b/thys/Automatic_Refinement/Parametricity/Relators.thy --- a/thys/Automatic_Refinement/Parametricity/Relators.thy +++ b/thys/Automatic_Refinement/Parametricity/Relators.thy @@ -1,992 +1,991 @@ section \Relators\ theory Relators imports "../Lib/Refine_Lib" begin text \ We define the concept of relators. The relation between a concrete type and an abstract type is expressed by a relation of type \('c\'a) set\. For each composed type, say \'a list\, we can define a {\em relator}, that takes as argument a relation for the element type, and returns a relation for the list type. For most datatypes, there exists a {\em natural relator}. For algebraic datatypes, this is the relator that preserves the structure of the datatype, and changes the components. For example, \list_rel::('c\'a) set \ ('c list\'a list) set\ is the natural relator for lists. However, relators can also be used to change the representation, and thus relate an implementation with an abstract type. For example, the relator \list_set_rel::('c\'a) set \ ('c list\'a set) set\ relates lists with the set of their elements. In this theory, we define some basic notions for relators, and then define natural relators for all HOL-types, including the function type. For each relator, we also show a single-valuedness property, and initialize a solver for single-valued properties. \ subsection \Basic Definitions\ text \ For smoother handling of relator unification, we require relator arguments to be applied by a special operator, such that we avoid higher-order unification problems. We try to set up some syntax to make this more transparent, and give relators a type-like prefix-syntax. \ definition relAPP :: "(('c1\'a1) set \ _) \ ('c1\'a1) set \ _" where "relAPP f x \ f x" syntax "_rel_APP" :: "args \ 'a \ 'b" ("\_\_" [0,900] 900) translations "\x,xs\R" == "\xs\(CONST relAPP R x)" "\x\R" == "CONST relAPP R x" ML \ structure Refine_Relators_Thms = struct structure rel_comb_def_rules = Named_Thms ( val name = @{binding refine_rel_defs} val description = "Refinement Framework: " ^ "Relator definitions" ); end \ setup Refine_Relators_Thms.rel_comb_def_rules.setup subsection \Basic HOL Relators\ subsubsection \Function\ definition fun_rel where fun_rel_def_internal: "fun_rel A B \ { (f,f'). \(a,a')\A. (f a, f' a')\B }" abbreviation fun_rel_syn (infixr "\" 60) where "A\B \ \A,B\fun_rel" lemma fun_rel_def[refine_rel_defs]: "A\B \ { (f,f'). \(a,a')\A. (f a, f' a')\B }" by (simp add: relAPP_def fun_rel_def_internal) lemma fun_relI[intro!]: "\\a a'. (a,a')\A \ (f a,f' a')\B\ \ (f,f')\A\B" by (auto simp: fun_rel_def) lemma fun_relD: shows " ((f,f')\(A\B)) \ (\x x'. \ (x,x')\A \ \ (f x, f' x')\B)" apply rule by (auto simp: fun_rel_def) lemma fun_relD1: assumes "(f,f')\Ra\Rr" assumes "f x = r" shows "\x'. (x,x')\Ra \ (r,f' x')\Rr" using assms by (auto simp: fun_rel_def) lemma fun_relD2: assumes "(f,f')\Ra\Rr" assumes "f' x' = r'" shows "\x. (x,x')\Ra \ (f x,r')\Rr" using assms by (auto simp: fun_rel_def) lemma fun_relE1: assumes "(f,f')\Id \ Rv" assumes "t' = f' x" shows "(f x,t')\Rv" using assms by (auto elim: fun_relD) lemma fun_relE2: assumes "(f,f')\Id \ Rv" assumes "t = f x" shows "(t,f' x)\Rv" using assms by (auto elim: fun_relD) subsubsection \Terminal Types\ abbreviation unit_rel :: "(unit\unit) set" where "unit_rel == Id" abbreviation "nat_rel \ Id::(nat\_) set" abbreviation "int_rel \ Id::(int\_) set" abbreviation "bool_rel \ Id::(bool\_) set" subsubsection \Product\ definition prod_rel where prod_rel_def_internal: "prod_rel R1 R2 \ { ((a,b),(a',b')) . (a,a')\R1 \ (b,b')\R2 }" abbreviation prod_rel_syn (infixr "\\<^sub>r" 70) where "a\\<^sub>rb \ \a,b\prod_rel" lemma prod_rel_def[refine_rel_defs]: "(\R1,R2\prod_rel) \ { ((a,b),(a',b')) . (a,a')\R1 \ (b,b')\R2 }" by (simp add: prod_rel_def_internal relAPP_def) lemma prod_relI: "\(a,a')\R1; (b,b')\R2\ \ ((a,b),(a',b'))\\R1,R2\prod_rel" by (auto simp: prod_rel_def) lemma prod_relE: assumes "(p,p')\\R1,R2\prod_rel" obtains a b a' b' where "p=(a,b)" and "p'=(a',b')" and "(a,a')\R1" and "(b,b')\R2" using assms by (auto simp: prod_rel_def) lemma prod_rel_simp[simp]: "((a,b),(a',b'))\\R1,R2\prod_rel \ (a,a')\R1 \ (b,b')\R2" by (auto intro: prod_relI elim: prod_relE) lemma in_Domain_prod_rel_iff[iff]: "(a,b)\Domain (A\\<^sub>rB) \ a\Domain A \ b\Domain B" by (auto simp: prod_rel_def) lemma prod_rel_comp: "(A \\<^sub>r B) O (C \\<^sub>r D) = (A O C) \\<^sub>r (B O D)" unfolding prod_rel_def by auto subsubsection \Option\ definition option_rel where option_rel_def_internal: "option_rel R \ { (Some a,Some a') | a a'. (a,a')\R } \ {(None,None)}" lemma option_rel_def[refine_rel_defs]: "\R\option_rel \ { (Some a,Some a') | a a'. (a,a')\R } \ {(None,None)}" by (simp add: option_rel_def_internal relAPP_def) lemma option_relI: "(None,None)\\R\ option_rel" "\ (a,a')\R \ \ (Some a, Some a')\\R\option_rel" by (auto simp: option_rel_def) lemma option_relE: assumes "(x,x')\\R\option_rel" obtains "x=None" and "x'=None" | a a' where "x=Some a" and "x'=Some a'" and "(a,a')\R" using assms by (auto simp: option_rel_def) lemma option_rel_simp[simp]: "(None,a)\\R\option_rel \ a=None" "(c,None)\\R\option_rel \ c=None" "(Some x,Some y)\\R\option_rel \ (x,y)\R" by (auto intro: option_relI elim: option_relE) subsubsection \Sum\ definition sum_rel where sum_rel_def_internal: "sum_rel Rl Rr \ { (Inl a, Inl a') | a a'. (a,a')\Rl } \ { (Inr a, Inr a') | a a'. (a,a')\Rr }" lemma sum_rel_def[refine_rel_defs]: "\Rl,Rr\sum_rel \ { (Inl a, Inl a') | a a'. (a,a')\Rl } \ { (Inr a, Inr a') | a a'. (a,a')\Rr }" by (simp add: sum_rel_def_internal relAPP_def) lemma sum_rel_simp[simp]: "\a a'. (Inl a, Inl a') \ \Rl,Rr\sum_rel \ (a,a')\Rl" "\a a'. (Inr a, Inr a') \ \Rl,Rr\sum_rel \ (a,a')\Rr" "\a a'. (Inl a, Inr a') \ \Rl,Rr\sum_rel" "\a a'. (Inr a, Inl a') \ \Rl,Rr\sum_rel" unfolding sum_rel_def by auto lemma sum_relI: "(l,l')\Rl \ (Inl l, Inl l') \ \Rl,Rr\sum_rel" "(r,r')\Rr \ (Inr r, Inr r') \ \Rl,Rr\sum_rel" by simp_all lemma sum_relE: assumes "(x,x')\\Rl,Rr\sum_rel" obtains l l' where "x=Inl l" and "x'=Inl l'" and "(l,l')\Rl" | r r' where "x=Inr r" and "x'=Inr r'" and "(r,r')\Rr" using assms by (auto simp: sum_rel_def) subsubsection \Lists\ definition list_rel where list_rel_def_internal: "list_rel R \ {(l,l'). list_all2 (\x x'. (x,x')\R) l l'}" lemma list_rel_def[refine_rel_defs]: "\R\list_rel \ {(l,l'). list_all2 (\x x'. (x,x')\R) l l'}" by (simp add: list_rel_def_internal relAPP_def) lemma list_rel_induct[induct set,consumes 1, case_names Nil Cons]: assumes "(l,l')\\R\ list_rel" assumes "P [] []" assumes "\x x' l l'. \ (x,x')\R; (l,l')\\R\list_rel; P l l' \ \ P (x#l) (x'#l')" shows "P l l'" using assms unfolding list_rel_def apply simp by (rule list_all2_induct) lemma list_rel_eq_listrel: "list_rel = listrel" apply (rule ext) apply safe proof goal_cases case (1 x a b) thus ?case unfolding list_rel_def_internal apply simp apply (induct a b rule: list_all2_induct) apply (auto intro: listrel.intros) done next case 2 thus ?case apply (induct) apply (auto simp: list_rel_def_internal) done qed lemma list_relI: "([],[])\\R\list_rel" "\ (x,x')\R; (l,l')\\R\list_rel \ \ (x#l,x'#l')\\R\list_rel" by (auto simp: list_rel_def) lemma list_rel_simp[simp]: "([],l')\\R\list_rel \ l'=[]" "(l,[])\\R\list_rel \ l=[]" "([],[])\\R\list_rel" "(x#l,x'#l')\\R\list_rel \ (x,x')\R \ (l,l')\\R\list_rel" by (auto simp: list_rel_def) lemma list_relE1: assumes "(l,[])\\R\list_rel" obtains "l=[]" using assms by auto lemma list_relE2: assumes "([],l)\\R\list_rel" obtains "l=[]" using assms by auto lemma list_relE3: assumes "(x#xs,l')\\R\list_rel" obtains x' xs' where "l'=x'#xs'" and "(x,x')\R" and "(xs,xs')\\R\list_rel" using assms apply (cases l') apply auto done lemma list_relE4: assumes "(l,x'#xs')\\R\list_rel" obtains x xs where "l=x#xs" and "(x,x')\R" and "(xs,xs')\\R\list_rel" using assms apply (cases l) apply auto done lemmas list_relE = list_relE1 list_relE2 list_relE3 list_relE4 lemma list_rel_imp_same_length: "(l, l') \ \R\list_rel \ length l = length l'" unfolding list_rel_eq_listrel relAPP_def by (rule listrel_eq_len) lemma list_rel_split_right_iff: "(x#xs,l)\\R\list_rel \ (\y ys. l=y#ys \ (x,y)\R \ (xs,ys)\\R\list_rel)" by (cases l) auto lemma list_rel_split_left_iff: "(l,y#ys)\\R\list_rel \ (\x xs. l=x#xs \ (x,y)\R \ (xs,ys)\\R\list_rel)" by (cases l) auto subsubsection \Sets\ text \Pointwise refinement: The abstract set is the image of the concrete set, and the concrete set only contains elements that have an abstract counterpart\ definition set_rel where set_rel_def_internal: "set_rel R \ {(A,B). (\x\A. \y\B. (x,y)\R) \ (\y\B. \x\A. (x,y)\R)}" term set_rel lemma set_rel_def[refine_rel_defs]: "\R\set_rel \ {(A,B). (\x\A. \y\B. (x,y)\R) \ (\y\B. \x\A. (x,y)\R)}" by (simp add: set_rel_def_internal relAPP_def) lemma set_rel_alt: "\R\set_rel = {(A,B). A \ R\``B \ B \ R``A}" unfolding set_rel_def by auto lemma set_relI[intro?]: assumes "\x. x\A \ \y\B. (x,y)\R" assumes "\y. y\B \ \x\A. (x,y)\R" shows "(A,B)\\R\set_rel" using assms unfolding set_rel_def by blast text \Original definition of \set_rel\ in refinement framework. Abandoned in favour of more symmetric definition above: \ definition old_set_rel where old_set_rel_def_internal: "old_set_rel R \ {(S,S'). S'=R``S \ S\Domain R}" lemma old_set_rel_def[refine_rel_defs]: "\R\old_set_rel \ {(S,S'). S'=R``S \ S\Domain R}" by (simp add: old_set_rel_def_internal relAPP_def) text \Old definition coincides with new definition for single-valued element relations. This is probably the reason why the old definition worked for most applications.\ lemma old_set_rel_sv_eq: "single_valued R \ \R\old_set_rel = \R\set_rel" unfolding set_rel_def old_set_rel_def single_valued_def by blast lemma set_rel_simp[simp]: "({},{})\\R\set_rel" by (auto simp: set_rel_def) lemma set_rel_empty_iff[simp]: "({},y)\\A\set_rel \ y={}" "(x,{})\\A\set_rel \ x={}" by (auto simp: set_rel_def; fastforce)+ lemma set_relD1: "(s,s')\\R\set_rel \ x\s \ \x'\s'. (x,x')\R" unfolding set_rel_def by blast lemma set_relD2: "(s,s')\\R\set_rel \ x'\s' \ \x\s. (x,x')\R" unfolding set_rel_def by blast lemma set_relE1[consumes 2]: assumes "(s,s')\\R\set_rel" "x\s" obtains x' where "x'\s'" "(x,x')\R" using set_relD1[OF assms] .. lemma set_relE2[consumes 2]: assumes "(s,s')\\R\set_rel" "x'\s'" obtains x where "x\s" "(x,x')\R" using set_relD2[OF assms] .. subsection \Automation\ subsubsection \A solver for relator properties\ lemma relprop_triggers: "\R. single_valued R \ single_valued R" "\R. R=Id \ R=Id" "\R. R=Id \ Id=R" "\R. Range R = UNIV \ Range R = UNIV" "\R. Range R = UNIV \ UNIV = Range R" "\R R'. R\R' \ R\R'" by auto ML \ structure relator_props = Named_Thms ( val name = @{binding relator_props} val description = "Additional relator properties" ) structure solve_relator_props = Named_Thms ( val name = @{binding solve_relator_props} val description = "Relator properties that solve goal" ) \ setup relator_props.setup setup solve_relator_props.setup declaration \ Tagged_Solver.declare_solver @{thms relprop_triggers} @{binding relator_props_solver} "Additional relator properties solver" (fn ctxt => (REPEAT_ALL_NEW (CHANGED o ( match_tac ctxt (solve_relator_props.get ctxt) ORELSE' match_tac ctxt (relator_props.get ctxt) )))) \ declaration \ Tagged_Solver.declare_solver [] @{binding force_relator_props_solver} "Additional relator properties solver (instantiate schematics)" (fn ctxt => (REPEAT_ALL_NEW (CHANGED o ( resolve_tac ctxt (solve_relator_props.get ctxt) ORELSE' match_tac ctxt (relator_props.get ctxt) )))) \ lemma relprop_id_orient[relator_props]: "R=Id \ Id=R" and relprop_eq_refl[solve_relator_props]: "t = t" by auto lemma relprop_UNIV_orient[relator_props]: "R=UNIV \ UNIV=R" by auto subsubsection \ML-Level utilities\ ML \ signature RELATORS = sig val mk_relT: typ * typ -> typ val dest_relT: typ -> typ * typ val mk_relAPP: term -> term -> term val list_relAPP: term list -> term -> term val strip_relAPP: term -> term list * term val mk_fun_rel: term -> term -> term val list_rel: term list -> term -> term val rel_absT: term -> typ val rel_concT: term -> typ val mk_prodrel: term * term -> term val is_prodrel: term -> bool val dest_prodrel: term -> term * term val strip_prodrel_left: term -> term list val list_prodrel_left: term list -> term val declare_natural_relator: (string*string) -> Context.generic -> Context.generic val remove_natural_relator: string -> Context.generic -> Context.generic val natural_relator_of: Proof.context -> string -> string option val mk_natural_relator: Proof.context -> term list -> string -> term option val setup: theory -> theory end structure Relators :RELATORS = struct val mk_relT = HOLogic.mk_prodT #> HOLogic.mk_setT fun dest_relT (Type (@{type_name set},[Type (@{type_name prod},[cT,aT])])) = (cT,aT) | dest_relT ty = raise TYPE ("dest_relT",[ty],[]) fun mk_relAPP x f = let val xT = fastype_of x val fT = fastype_of f val rT = range_type fT in Const (@{const_name relAPP},fT-->xT-->rT)$f$x end val list_relAPP = fold mk_relAPP fun strip_relAPP R = let fun aux @{mpat "\?R\?S"} l = aux S (R::l) | aux R l = (l,R) in aux R [] end val rel_absT = fastype_of #> HOLogic.dest_setT #> HOLogic.dest_prodT #> snd val rel_concT = fastype_of #> HOLogic.dest_setT #> HOLogic.dest_prodT #> fst fun mk_fun_rel r1 r2 = let val (r1T,r2T) = (fastype_of r1,fastype_of r2) val (c1T,a1T) = dest_relT r1T val (c2T,a2T) = dest_relT r2T val (cT,aT) = (c1T --> c2T, a1T --> a2T) val rT = mk_relT (cT,aT) in list_relAPP [r1,r2] (Const (@{const_name fun_rel},r1T-->r2T-->rT)) end val list_rel = fold_rev mk_fun_rel fun mk_prodrel (A,B) = @{mk_term "?A \\<^sub>r ?B"} fun is_prodrel @{mpat "_ \\<^sub>r _"} = true | is_prodrel _ = false fun dest_prodrel @{mpat "?A \\<^sub>r ?B"} = (A,B) | dest_prodrel t = raise TERM("dest_prodrel",[t]) fun strip_prodrel_left @{mpat "?A \\<^sub>r ?B"} = strip_prodrel_left A @ [B] | strip_prodrel_left @{mpat (typs) "unit_rel"} = [] | strip_prodrel_left R = [R] val list_prodrel_left = Refine_Util.list_binop_left @{term unit_rel} mk_prodrel structure natural_relators = Generic_Data ( type T = string Symtab.table val empty = Symtab.empty val merge = Symtab.join (fn _ => fn (_,cn) => cn) ) fun declare_natural_relator tcp = natural_relators.map (Symtab.update tcp) fun remove_natural_relator tname = natural_relators.map (Symtab.delete_safe tname) fun natural_relator_of ctxt = Symtab.lookup (natural_relators.get (Context.Proof ctxt)) (* [R1,\,Rn] T is mapped to \R1,\,Rn\ Trel *) fun mk_natural_relator ctxt args Tname = case natural_relator_of ctxt Tname of NONE => NONE | SOME Cname => SOME let val argsT = map fastype_of args val (cTs, aTs) = map dest_relT argsT |> split_list val aT = Type (Tname,aTs) val cT = Type (Tname,cTs) val rT = mk_relT (cT,aT) in list_relAPP args (Const (Cname,argsT--->rT)) end fun natural_relator_from_term (t as Const (name,T)) = let fun err msg = raise TERM (msg,[t]) val (argTs,bodyT) = strip_type T val (conTs,absTs) = argTs |> map (HOLogic.dest_setT #> HOLogic.dest_prodT) |> split_list val (bconT,babsT) = bodyT |> HOLogic.dest_setT |> HOLogic.dest_prodT val (Tcon,bconTs) = dest_Type bconT val (Tcon',babsTs) = dest_Type babsT val _ = Tcon = Tcon' orelse err "Type constructors do not match" val _ = conTs = bconTs orelse err "Concrete types do not match" val _ = absTs = babsTs orelse err "Abstract types do not match" in (Tcon,name) end | natural_relator_from_term t = raise TERM ("Expected constant",[t]) (* TODO: Localize this! *) local fun decl_natrel_aux t context = let fun warn msg = let val tP = Context.cases Syntax.pretty_term_global Syntax.pretty_term context t val m = Pretty.block [ Pretty.str "Ignoring invalid natural_relator declaration:", Pretty.brk 1, Pretty.str msg, Pretty.brk 1, tP ] |> Pretty.string_of val _ = warning m in context end in - declare_natural_relator (natural_relator_from_term t) context - handle - TERM (msg,_) => warn msg - | exn => if Exn.is_interrupt exn then Exn.reraise exn else warn "" + \<^try>\declare_natural_relator (natural_relator_from_term t) context + catch TERM (msg,_) => warn msg + | exn => warn ""\ end in val natural_relator_attr = Scan.repeat1 Args.term >> (fn ts => Thm.declaration_attribute ( fn _ => fold decl_natrel_aux ts) ) end val setup = I #> Attrib.setup @{binding natural_relator} natural_relator_attr "Declare natural relator" end \ setup Relators.setup subsection \Setup\ subsubsection "Natural Relators" declare [[natural_relator unit_rel int_rel nat_rel bool_rel fun_rel prod_rel option_rel sum_rel list_rel ]] (*declaration {* let open Relators in fn _ => declare_natural_relator (@{type_name unit},@{const_name unit_rel}) #> declare_natural_relator (@{type_name fun},@{const_name fun_rel}) #> declare_natural_relator (@{type_name prod},@{const_name prod_rel}) #> declare_natural_relator (@{type_name option},@{const_name option_rel}) #> declare_natural_relator (@{type_name sum},@{const_name sum_rel}) #> declare_natural_relator (@{type_name list},@{const_name list_rel}) end *}*) ML_val \ Relators.mk_natural_relator @{context} [@{term "Ra::('c\'a) set"},@{term "\Rb\option_rel"}] @{type_name prod} |> the |> Thm.cterm_of @{context} ; Relators.mk_fun_rel @{term "\Id\option_rel"} @{term "\Id\list_rel"} |> Thm.cterm_of @{context} \ subsubsection "Additional Properties" lemmas [relator_props] = single_valued_Id subset_refl refl (* TODO: Move *) lemma eq_UNIV_iff: "S=UNIV \ (\x. x\S)" by auto lemma fun_rel_sv[relator_props]: assumes RAN: "Range Ra = UNIV" assumes SV: "single_valued Rv" shows "single_valued (Ra \ Rv)" proof (intro single_valuedI ext impI allI) fix f g h x' assume R1: "(f,g)\Ra\Rv" and R2: "(f,h)\Ra\Rv" from RAN obtain x where AR: "(x,x')\Ra" by auto from fun_relD[OF R1 AR] have "(f x,g x') \ Rv" . moreover from fun_relD[OF R2 AR] have "(f x,h x') \ Rv" . ultimately show "g x' = h x'" using SV by (auto dest: single_valuedD) qed lemmas [relator_props] = Range_Id lemma fun_rel_id[relator_props]: "\R1=Id; R2=Id\ \ R1 \ R2 = Id" by (auto simp: fun_rel_def) lemma fun_rel_id_simp[simp]: "Id\Id = Id" by tagged_solver lemma fun_rel_comp_dist[relator_props]: "(R1\R2) O (R3\R4) \ ((R1 O R3) \ (R2 O R4))" by (auto simp: fun_rel_def) lemma fun_rel_mono[relator_props]: "\ R1\R2; R3\R4 \ \ R2\R3 \ R1\R4" by (force simp: fun_rel_def) lemma prod_rel_sv[relator_props]: "\single_valued R1; single_valued R2\ \ single_valued (\R1,R2\prod_rel)" by (auto intro: single_valuedI dest: single_valuedD simp: prod_rel_def) lemma prod_rel_id[relator_props]: "\R1=Id; R2=Id\ \ \R1,R2\prod_rel = Id" by (auto simp: prod_rel_def) lemma prod_rel_id_simp[simp]: "\Id,Id\prod_rel = Id" by tagged_solver lemma prod_rel_mono[relator_props]: "\ R2\R1; R3\R4 \ \ \R2,R3\prod_rel \ \R1,R4\prod_rel" by (auto simp: prod_rel_def) lemma prod_rel_range[relator_props]: "\Range Ra=UNIV; Range Rb=UNIV\ \ Range (\Ra,Rb\prod_rel) = UNIV" apply (auto simp: prod_rel_def) by (metis Range_iff UNIV_I)+ lemma option_rel_sv[relator_props]: "\single_valued R\ \ single_valued (\R\option_rel)" by (auto intro: single_valuedI dest: single_valuedD simp: option_rel_def) lemma option_rel_id[relator_props]: "R=Id \ \R\option_rel = Id" by (auto simp: option_rel_def) lemma option_rel_id_simp[simp]: "\Id\option_rel = Id" by tagged_solver lemma option_rel_mono[relator_props]: "R\R' \ \R\option_rel \ \R'\option_rel" by (auto simp: option_rel_def) lemma option_rel_range: "Range R = UNIV \ Range (\R\option_rel) = UNIV" apply (auto simp: option_rel_def Range_iff) by (metis Range_iff UNIV_I option.exhaust) lemma option_rel_inter[simp]: "\R1 \ R2\option_rel = \R1\option_rel \ \R2\option_rel" by (auto simp: option_rel_def) lemma option_rel_constraint[simp]: "(x,x)\\UNIV\C\option_rel \ (\v. x=Some v \ v\C)" by (auto simp: option_rel_def) lemma sum_rel_sv[relator_props]: "\single_valued Rl; single_valued Rr\ \ single_valued (\Rl,Rr\sum_rel)" by (auto intro: single_valuedI dest: single_valuedD simp: sum_rel_def) lemma sum_rel_id[relator_props]: "\Rl=Id; Rr=Id\ \ \Rl,Rr\sum_rel = Id" apply (auto elim: sum_relE) apply (case_tac b) apply simp_all done lemma sum_rel_id_simp[simp]: "\Id,Id\sum_rel = Id" by tagged_solver lemma sum_rel_mono[relator_props]: "\ Rl\Rl'; Rr\Rr' \ \ \Rl,Rr\sum_rel \ \Rl',Rr'\sum_rel" by (auto simp: sum_rel_def) lemma sum_rel_range[relator_props]: "\ Range Rl=UNIV; Range Rr=UNIV \ \ Range (\Rl,Rr\sum_rel) = UNIV" apply (auto simp: sum_rel_def Range_iff) by (metis Range_iff UNIV_I sumE) lemma list_rel_sv_iff: "single_valued (\R\list_rel) \ single_valued R" apply (intro iffI[rotated] single_valuedI allI impI) apply (clarsimp simp: list_rel_def) proof - fix x y z assume SV: "single_valued R" assume "list_all2 (\x x'. (x, x') \ R) x y" and "list_all2 (\x x'. (x, x') \ R) x z" thus "y=z" apply (induct arbitrary: z rule: list_all2_induct) apply simp apply (case_tac z) apply force apply (force intro: single_valuedD[OF SV]) done next fix x y z assume SV: "single_valued (\R\list_rel)" assume "(x,y)\R" "(x,z)\R" hence "([x],[y])\\R\list_rel" and "([x],[z])\\R\list_rel" by (auto simp: list_rel_def) with single_valuedD[OF SV] show "y=z" by blast qed lemma list_rel_sv[relator_props]: "single_valued R \ single_valued (\R\list_rel)" by (simp add: list_rel_sv_iff) lemma list_rel_id[relator_props]: "\R=Id\ \ \R\list_rel = Id" by (auto simp add: list_rel_def list_all2_eq[symmetric]) lemma list_rel_id_simp[simp]: "\Id\list_rel = Id" by tagged_solver lemma list_rel_mono[relator_props]: assumes A: "R\R'" shows "\R\list_rel \ \R'\list_rel" proof clarsimp fix l l' assume "(l,l')\\R\list_rel" thus "(l,l')\\R'\list_rel" apply induct using A by auto qed lemma list_rel_range[relator_props]: assumes A: "Range R = UNIV" shows "Range (\R\list_rel) = UNIV" proof (clarsimp simp: eq_UNIV_iff) fix l show "l\Range (\R\list_rel)" apply (induct l) using A[unfolded eq_UNIV_iff] by (auto simp: Range_iff intro: list_relI) qed lemma bijective_imp_sv: "bijective R \ single_valued R" "bijective R \ single_valued (R\)" by (simp_all add: bijective_alt) (* TODO: Move *) declare bijective_Id[relator_props] declare bijective_Empty[relator_props] text \Pointwise refinement for set types:\ lemma set_rel_sv[relator_props]: "single_valued R \ single_valued (\R\set_rel)" unfolding single_valued_def set_rel_def by blast lemma set_rel_id[relator_props]: "R=Id \ \R\set_rel = Id" by (auto simp add: set_rel_def) lemma set_rel_id_simp[simp]: "\Id\set_rel = Id" by tagged_solver lemma set_rel_csv[relator_props]: "\ single_valued (R\) \ \ single_valued ((\R\set_rel)\)" unfolding single_valued_def set_rel_def converse_iff by fast subsection \Invariant and Abstraction\ text \ Quite often, a relation can be described as combination of an abstraction function and an invariant, such that the invariant describes valid values on the concrete domain, and the abstraction function maps valid concrete values to its corresponding abstract value. \ definition build_rel where "build_rel \ I \ {(c,a) . a=\ c \ I c}" abbreviation "br\build_rel" lemmas br_def[refine_rel_defs] = build_rel_def lemma in_br_conv: "(c,a)\br \ I \ a=\ c \ I c" by (auto simp: br_def) lemma brI[intro?]: "\ a=\ c; I c \ \ (c,a)\br \ I" by (simp add: br_def) lemma br_id[simp]: "br id (\_. True) = Id" unfolding build_rel_def by auto lemma br_chain: "(build_rel \ J) O (build_rel \ I) = build_rel (\\\) (\s. J s \ I (\ s))" unfolding build_rel_def by auto lemma br_sv[simp, intro!,relator_props]: "single_valued (br \ I)" unfolding build_rel_def apply (rule single_valuedI) apply auto done lemma converse_br_sv_iff[simp]: "single_valued (converse (br \ I)) \ inj_on \ (Collect I)" by (auto intro!: inj_onI single_valuedI dest: single_valuedD inj_onD simp: br_def) [] lemmas [relator_props] = single_valued_relcomp lemma br_comp_alt: "br \ I O R = { (c,a) . I c \ (\ c,a)\R }" by (auto simp add: br_def) lemma br_comp_alt': "{(c,a) . a=\ c \ I c} O R = { (c,a) . I c \ (\ c,a)\R }" by auto lemma single_valued_as_brE: assumes "single_valued R" obtains \ invar where "R=br \ invar" apply (rule that[of "\x. THE y. (x,y)\R" "\x. x\Domain R"]) using assms unfolding br_def by (auto dest: single_valuedD intro: the_equality[symmetric] theI) lemma sv_add_invar: "single_valued R \ single_valued {(c, a). (c, a) \ R \ I c}" by (auto dest: single_valuedD intro: single_valuedI) lemma br_Image_conv[simp]: "br \ I `` S = {\ x | x. x\S \ I x}" by (auto simp: br_def) subsection \Miscellanneous\ lemma rel_cong: "(f,g)\Id \ (x,y)\Id \ (f x, g y)\Id" by simp lemma rel_fun_cong: "(f,g)\Id \ (f x, g x)\Id" by simp lemma rel_arg_cong: "(x,y)\Id \ (f x, f y)\Id" by simp subsection \Conversion between Predicate and Set Based Relators\ text \ Autoref uses set-based relators of type @{typ \('a\'b) set\}, while the transfer and lifting package of Isabelle/HOL uses predicate based relators of type @{typ \'a \ 'b \ bool\}. This section defines some utilities to convert between the two. \ definition "rel2p R x y \ (x,y)\R" definition "p2rel P \ {(x,y). P x y}" lemma rel2pD: "\rel2p R a b\ \ (a,b)\R" by (auto simp: rel2p_def) lemma p2relD: "\(a,b) \ p2rel R\ \ R a b" by (auto simp: p2rel_def) lemma rel2p_inv[simp]: "rel2p (p2rel P) = P" "p2rel (rel2p R) = R" by (auto simp: rel2p_def[abs_def] p2rel_def) named_theorems rel2p named_theorems p2rel lemma rel2p_dflt[rel2p]: "rel2p Id = (=)" "rel2p (A\B) = rel_fun (rel2p A) (rel2p B)" "rel2p (A\\<^sub>rB) = rel_prod (rel2p A) (rel2p B)" "rel2p (\A,B\sum_rel) = rel_sum (rel2p A) (rel2p B)" "rel2p (\A\option_rel) = rel_option (rel2p A)" "rel2p (\A\list_rel) = list_all2 (rel2p A)" by (auto simp: rel2p_def[abs_def] intro!: ext simp: fun_rel_def rel_fun_def simp: sum_rel_def elim: rel_sum.cases simp: option_rel_def elim: option.rel_cases simp: list_rel_def simp: set_rel_def rel_set_def Image_def ) lemma p2rel_dflt[p2rel]: "p2rel (=) = Id" "p2rel (rel_fun A B) = p2rel A \ p2rel B" "p2rel (rel_prod A B) = p2rel A \\<^sub>r p2rel B" "p2rel (rel_sum A B) = \p2rel A, p2rel B\sum_rel" "p2rel (rel_option A) = \p2rel A\option_rel" "p2rel (list_all2 A) = \p2rel A\list_rel" by (auto simp: p2rel_def[abs_def] simp: fun_rel_def rel_fun_def simp: sum_rel_def elim: rel_sum.cases simp: option_rel_def elim: option.rel_cases simp: list_rel_def ) lemma [rel2p]: "rel2p (\A\set_rel) = rel_set (rel2p A)" unfolding set_rel_def rel_set_def rel2p_def[abs_def] by blast lemma [p2rel]: "left_unique A \ p2rel (rel_set A) = (\p2rel A\set_rel)" unfolding set_rel_def rel_set_def p2rel_def[abs_def] by blast lemma rel2p_comp: "rel2p A OO rel2p B = rel2p (A O B)" by (auto simp: rel2p_def[abs_def] intro!: ext) lemma rel2p_inj[simp]: "rel2p A = rel2p B \ A=B" by (auto simp: rel2p_def[abs_def]; meson) lemma rel2p_left_unique: "left_unique (rel2p A) = single_valued (A\)" unfolding left_unique_def rel2p_def single_valued_def by blast lemma rel2p_right_unique: "right_unique (rel2p A) = single_valued A" unfolding right_unique_def rel2p_def single_valued_def by blast lemma rel2p_bi_unique: "bi_unique (rel2p A) \ single_valued A \ single_valued (A\)" unfolding bi_unique_alt_def by (auto simp: rel2p_left_unique rel2p_right_unique) lemma p2rel_left_unique: "single_valued ((p2rel A)\) = left_unique A" unfolding left_unique_def p2rel_def single_valued_def by blast lemma p2rel_right_unique: "single_valued (p2rel A) = right_unique A" unfolding right_unique_def p2rel_def single_valued_def by blast subsection \More Properties\ (* TODO: Do compp-lemmas for other standard relations *) lemma list_rel_compp: "\A O B\list_rel = \A\list_rel O \B\list_rel" using list.rel_compp[of "rel2p A" "rel2p B"] by (auto simp: rel2p(2-)[symmetric] rel2p_comp) (* TODO: Not very systematic proof *) lemma option_rel_compp: "\A O B\option_rel = \A\option_rel O \B\option_rel" using option.rel_compp[of "rel2p A" "rel2p B"] by (auto simp: rel2p(2-)[symmetric] rel2p_comp) (* TODO: Not very systematic proof *) lemma prod_rel_compp: "\A O B, C O D\prod_rel = \A,C\prod_rel O \B,D\prod_rel" using prod.rel_compp[of "rel2p A" "rel2p B" "rel2p C" "rel2p D"] by (auto simp: rel2p(2-)[symmetric] rel2p_comp) (* TODO: Not very systematic proof *) lemma sum_rel_compp: "\A O B, C O D\sum_rel = \A,C\sum_rel O \B,D\sum_rel" using sum.rel_compp[of "rel2p A" "rel2p B" "rel2p C" "rel2p D"] by (auto simp: rel2p(2-)[symmetric] rel2p_comp) (* TODO: Not very systematic proof *) lemma set_rel_compp: "\A O B\set_rel = \A\set_rel O \B\set_rel" using rel_set_OO[of "rel2p A" "rel2p B"] by (auto simp: rel2p(2-)[symmetric] rel2p_comp) (* TODO: Not very systematic proof *) lemma map_in_list_rel_conv: shows "(l, map \ l) \ \br \ I\list_rel \ (\x\set l. I x)" by (induction l) (auto simp: in_br_conv) lemma br_set_rel_alt: "(s',s)\\br \ I\set_rel \ (s=\`s' \ (\x\s'. I x))" by (auto simp: set_rel_def br_def) (* TODO: Find proof that does not depend on br, and move to Misc *) lemma finite_Image_sv: "single_valued R \ finite s \ finite (R``s)" by (erule single_valued_as_brE) simp lemma finite_set_rel_transfer: "\(s,s')\\R\set_rel; single_valued R; finite s\ \ finite s'" unfolding set_rel_alt by (blast intro: finite_subset[OF _ finite_Image_sv]) lemma finite_set_rel_transfer_back: "\(s,s')\\R\set_rel; single_valued (R\); finite s'\ \ finite s" unfolding set_rel_alt by (blast intro: finite_subset[OF _ finite_Image_sv]) end diff --git a/thys/Dict_Construction/dict_construction_util.ML b/thys/Dict_Construction/dict_construction_util.ML --- a/thys/Dict_Construction/dict_construction_util.ML +++ b/thys/Dict_Construction/dict_construction_util.ML @@ -1,316 +1,316 @@ infixr 5 ==> infixr ===> infix 1 CONTINUE_WITH CONTINUE_WITH_FW signature DICT_CONSTRUCTION_UTIL = sig (* general *) val split_list3: ('a * 'b * 'c) list -> 'a list * 'b list * 'c list val symreltab_of_symtab: 'a Symtab.table Symtab.table -> 'a Symreltab.table val zip_symtabs: ('a -> 'b -> 'c) -> 'a Symtab.table -> 'b Symtab.table -> 'c Symtab.table val cat_options: 'a option list -> 'a list val partition: ('a -> bool) -> 'a list -> 'a list * 'a list val unappend: 'a list * 'b -> 'c list -> 'c list * 'c list val flat_right: ('a * 'b list) list -> ('a * 'b) list (* logic *) val ===> : term list * term -> term val ==> : term * term -> term val sortify: sort -> term -> term val sortify_typ: sort -> typ -> typ val typify: term -> term val typify_typ: typ -> typ val all_frees: term -> (string * typ) list val all_frees': term -> string list val all_tfrees: typ -> (string * sort) list (* printing *) val pretty_const: Proof.context -> string -> Pretty.T (* conversion/tactic *) val ANY: tactic list -> tactic val ANY': ('a -> tactic) list -> 'a -> tactic val CONTINUE_WITH: (int -> tactic) * (int -> tactic) list -> int -> thm -> thm Seq.seq val CONTINUE_WITH_FW: (int -> tactic) * (int -> tactic) list -> int -> thm -> thm Seq.seq val SOLVED: tactic -> tactic val TRY': ('a -> tactic) -> 'a -> tactic val descend_fun_conv: conv -> conv val lhs_conv: conv -> conv val rhs_conv: conv -> conv val rewr_lhs_head_conv: thm -> conv val rewr_rhs_head_conv: thm -> conv val conv_result: ('a -> thm) -> 'a -> term val changed_conv: ('a -> thm) -> 'a -> thm val maybe_induct_tac: thm list option -> term list list -> term list list -> Proof.context -> tactic val multi_induct_tac: thm list -> term list list -> term list list -> Proof.context -> tactic val print_tac': Proof.context -> string -> int -> tactic val fo_cong_tac: Proof.context -> thm -> int -> tactic (* theorem manipulation *) val contract: Proof.context -> thm -> thm val on_thms_complete: (unit -> 'a) -> thm list -> thm list (* theory *) val define_params_nosyn: term -> local_theory -> thm * local_theory val note_thm: binding -> thm -> local_theory -> thm * local_theory val note_thms: binding -> thm list -> local_theory -> thm list * local_theory (* timing *) val with_timeout: Time.time -> ('a -> 'a) -> 'a -> 'a (* debugging *) val debug: bool Config.T val if_debug: Proof.context -> (unit -> unit) -> unit val ALLGOALS': Proof.context -> (int -> tactic) -> tactic val prove': Proof.context -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm val prove_common': Proof.context -> string list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> thm list end structure Dict_Construction_Util : DICT_CONSTRUCTION_UTIL = struct (* general *) fun symreltab_of_symtab tab = Symtab.map (K Symtab.dest) tab |> Symtab.dest |> maps (fn (k, kvs) => map (apfst (pair k)) kvs) |> Symreltab.make fun split_list3 [] = ([], [], []) | split_list3 ((x, y, z) :: rest) = let val (xs, ys, zs) = split_list3 rest in (x :: xs, y :: ys, z :: zs) end fun zip_symtabs f t1 t2 = let open Symtab val ord = fast_string_ord fun aux acc [] [] = acc | aux acc ((k1, x) :: xs) ((k2, y) :: ys) = (case ord (k1, k2) of EQUAL => aux (update_new (k1, f x y) acc) xs ys | LESS => raise UNDEF k1 | GREATER => raise UNDEF k2) | aux _ ((k, _) :: _) [] = raise UNDEF k | aux _ [] ((k, _) :: _) = raise UNDEF k in aux empty (dest t1) (dest t2) end fun cat_options [] = [] | cat_options (SOME x :: xs) = x :: cat_options xs | cat_options (NONE :: xs) = cat_options xs fun partition f xs = (filter f xs, filter_out f xs) fun unappend (xs, _) = chop (length xs) fun flat_right [] = [] | flat_right ((x, ys) :: rest) = map (pair x) ys @ flat_right rest (* logic *) fun x ==> y = Logic.mk_implies (x, y) val op ===> = Library.foldr op ==> fun sortify_typ sort (Type (tyco, args)) = Type (tyco, map (sortify_typ sort) args) | sortify_typ sort (TFree (name, _)) = TFree (name, sort) | sortify_typ _ (TVar _) = error "TVar encountered" fun sortify sort (Const (name, typ)) = Const (name, sortify_typ sort typ) | sortify sort (Free (name, typ)) = Free (name, sortify_typ sort typ) | sortify sort (t $ u) = sortify sort t $ sortify sort u | sortify sort (Abs (name, typ, term)) = Abs (name, sortify_typ sort typ, sortify sort term) | sortify _ (Bound n) = Bound n | sortify _ (Var _) = error "Var encountered" val typify_typ = sortify_typ @{sort type} val typify = sortify @{sort type} fun all_frees (Free (name, typ)) = [(name, typ)] | all_frees (t $ u) = union (op =) (all_frees t) (all_frees u) | all_frees (Abs (_, _, t)) = all_frees t | all_frees _ = [] val all_frees' = map fst o all_frees fun all_tfrees (TFree (name, sort)) = [(name, sort)] | all_tfrees (Type (_, ts)) = fold (union (op =)) (map all_tfrees ts) [] | all_tfrees _ = [] (* printing *) fun pretty_const ctxt const = Syntax.pretty_term ctxt (Const (const, Sign.the_const_type (Proof_Context.theory_of ctxt) const)) (* conversion/tactic *) fun ANY tacs = fold (curry op APPEND) tacs no_tac fun ANY' tacs n = fold (curry op APPEND) (map (fn t => t n) tacs) no_tac fun TRY' tac n = TRY (tac n) fun descend_fun_conv cv = cv else_conv (fn ct => case Thm.term_of ct of _ $ _ => Conv.fun_conv (descend_fun_conv cv) ct | _ => Conv.no_conv ct) fun lhs_conv cv = cv |> Conv.arg1_conv |> Conv.arg_conv fun rhs_conv cv = cv |> Conv.arg_conv |> Conv.arg_conv fun rewr_lhs_head_conv thm = safe_mk_meta_eq thm |> Conv.rewr_conv |> descend_fun_conv |> lhs_conv fun rewr_rhs_head_conv thm = safe_mk_meta_eq thm |> Conv.rewr_conv |> descend_fun_conv |> rhs_conv fun conv_result cv ct = Thm.prop_of (cv ct) |> Logic.dest_equals |> snd fun changed_conv cv = fn ct => let val res = cv ct val (lhs, rhs) = Thm.prop_of res |> Logic.dest_equals in if lhs aconv rhs then raise CTERM ("no conversion", []) else res end fun multi_induct_tac rules insts arbitrary ctxt = let val insts' = map (map (SOME o pair NONE o rpair false)) insts val arbitrary' = map (map dest_Free) arbitrary in DETERM (Induct.induct_tac ctxt false insts' arbitrary' [] (SOME rules) [] 1) end fun maybe_induct_tac (SOME rules) insts arbitrary = multi_induct_tac rules insts arbitrary | maybe_induct_tac NONE _ _ = K all_tac fun (tac CONTINUE_WITH tacs) i st = st |> (tac i THEN (fn st' => let val n' = Thm.nprems_of st' val n = Thm.nprems_of st fun aux [] _ = all_tac | aux (tac :: tacs) i = tac i THEN aux tacs (i - 1) in if n' - n + 1 <> length tacs then raise THM ("CONTINUE_WITH: unexpected number of emerging subgoals", 0, [st']) else aux (rev tacs) (i + n' - n) st' end)) fun (tac CONTINUE_WITH_FW tacs) i st = st |> (tac i THEN (fn st' => let val n' = Thm.nprems_of st' val n = Thm.nprems_of st fun aux [] _ st = all_tac st | aux (tac :: tacs) i st = st |> (tac i THEN (fn st' => aux tacs (i + 1 + Thm.nprems_of st' - Thm.nprems_of st) st')) in if n' - n + 1 <> length tacs then raise THM ("unexpected number of emerging subgoals", 0, [st']) else aux tacs i st' end)) fun SOLVED tac = tac THEN ALLGOALS (K no_tac) fun print_tac' ctxt str = SELECT_GOAL (print_tac ctxt str) fun fo_cong_tac ctxt thm = SUBGOAL (fn (concl, i) => let val lhs_of = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst val concl_pat = lhs_of (Thm.concl_of thm) |> Thm.cterm_of ctxt val concl = lhs_of concl |> Thm.cterm_of ctxt val insts = Thm.first_order_match (concl_pat, concl) in resolve_tac ctxt [Drule.instantiate_normalize insts thm] i end handle Pattern.MATCH => no_tac) (* theorem manipulation *) fun contract ctxt thm = let val (((_, frees), [thm']), ctxt') = Variable.import true [thm] ctxt val prop = Thm.prop_of thm' val prems = Logic.strip_imp_prems prop val (lhs, rhs) = Logic.strip_imp_concl prop |> HOLogic.dest_Trueprop |> HOLogic.dest_eq fun used x = exists (exists_subterm (fn t => t = x)) prems val (f, xs) = strip_comb lhs val (g, ys) = strip_comb rhs fun loop [] ys = (0, (f, list_comb (g, rev ys))) | loop xs [] = (0, (list_comb (f, rev xs), g)) | loop (x :: xs) (y :: ys) = if x = y andalso is_Free x andalso not (used x) then loop xs ys |> apfst (fn x => x + 1) else (0, (list_comb (f, rev (x :: xs)), list_comb (g, rev (y :: ys)))) val (count, (lhs', rhs')) = loop (rev xs) (rev ys) val concl' = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs')) fun tac ctxt 0 = resolve_tac ctxt [thm] THEN_ALL_NEW (Method.assm_tac ctxt) | tac ctxt n = resolve_tac ctxt @{thms ext} THEN' tac ctxt (n - 1) val prop = prems ===> concl' in Goal.prove_future ctxt' [] [] prop (fn {context, ...} => HEADGOAL (tac context count)) |> singleton (Variable.export ctxt' ctxt) end fun on_thms_complete f thms = (Future.fork (fn () => (Thm.consolidate thms; f ())); thms) (* theory *) fun define_params_nosyn term = Specification.definition NONE [] [] ((Binding.empty, []), term) #>> snd #>> snd fun note_thm binding thm = Local_Theory.note ((binding, []), [thm]) #>> snd #>> the_single fun note_thms binding thms = Local_Theory.note ((binding, []), thms) #>> snd (* timing *) fun with_timeout time f x = - case Exn.interruptible_capture (Timeout.apply time f) x of + case Exn.result (Timeout.apply time f) x of Exn.Res y => y | Exn.Exn (Timeout.TIMEOUT _) => x | Exn.Exn e => Exn.reraise e (* debugging *) val debug = Attrib.setup_config_bool @{binding "dict_construction_debug"} (K false) fun if_debug ctxt f = if Config.get ctxt debug then f () else () fun ALLGOALS' ctxt = if Config.get ctxt debug then ALLGOALS else PARALLEL_ALLGOALS fun prove' ctxt = if Config.get ctxt debug then Goal.prove ctxt else Goal.prove_future ctxt fun prove_common' ctxt = Goal.prove_common ctxt (if Config.get ctxt debug then NONE else SOME ~1) end \ No newline at end of file diff --git a/thys/Dict_Construction/transfer_termination.ML b/thys/Dict_Construction/transfer_termination.ML --- a/thys/Dict_Construction/transfer_termination.ML +++ b/thys/Dict_Construction/transfer_termination.ML @@ -1,154 +1,154 @@ signature TRANSFER_TERMINATION = sig val termination_tac: Function.info -> Function.info -> Proof.context -> int -> tactic end structure Transfer_Termination : TRANSFER_TERMINATION = struct open Dict_Construction_Util fun termination_tac ({R = new_R, ...}: Function.info) (old_info: Function.info) ctxt = let fun fallback_tac warn _ = (if warn then warning "Falling back to another termination proof" else (); Seq.empty) fun map_comp_bnf typ = let (* we start from a fresh lthy to avoid local hyps interfering with BNF *) val lthy = Proof_Context.theory_of ctxt |> Named_Target.theory_init |> Config.put BNF_Comp.typedef_threshold ~1 (* we just pretend that they're all live here *) val live_As = all_tfrees typ fun flatten_tyargs Ass = live_As |> filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) (* Dont_Inline would create new definitions, always *) val ((bnf, _), ((_, {map_unfolds, ...}), _)) = BNF_Comp.bnf_of_typ false BNF_Def.Do_Inline I flatten_tyargs live_As [] typ ((BNF_Comp.empty_comp_cache, BNF_Comp.empty_unfolds), lthy) val subst = map (Logic.dest_equals o Thm.prop_of) map_unfolds val t = BNF_Def.map_of_bnf bnf in (live_As, Envir.expand_term_defs dest_Const (map (apfst dest_Const) subst) t) end val tac = case old_info of {R = old_R, totality = SOME totality, ...} => let fun get_eq R = Inductive.the_inductive ctxt R |> snd |> #eqs |> the_single |> Local_Defs.abs_def_rule ctxt val (old_R_eq, new_R_eq) = apply2 get_eq (old_R, new_R) fun get_typ R = fastype_of R |> strip_type |> fst |> hd |> Type.legacy_freeze_type val (old_R_typ, new_R_typ) = apply2 get_typ (old_R, new_R) (* simple strategy: old_R and new_R are identical *) val simple_tac = let val totality' = Local_Defs.unfold ctxt [old_R_eq] totality in Local_Defs.unfold_tac ctxt [new_R_eq] THEN HEADGOAL (SOLVED' (resolve_tac ctxt [totality'])) end (* smart strategy: new_R can be simulated by old_R *) (* FIXME this is trigger-happy *) - val smart_tac = Exn.interruptible_capture (fn st => + val smart_tac = Exn.result (fn st => let val old_R_stripped = Thm.prop_of old_R_eq |> Logic.dest_equals |> snd |> map_types (K dummyT) |> Syntax.check_term ctxt val futile = old_R_stripped |> exists_type (exists_subtype (fn TFree (_, sort) => sort <> @{sort type} | TVar (_, sort) => sort <> @{sort type} | _ => false)) fun costrip_prodT new_t old_t = if Type.could_match (old_t, new_t) then (0, new_t) else case costrip_prodT (snd (HOLogic.dest_prodT new_t)) old_t of (n, stripped_t) => (n + 1, stripped_t) fun construct_inner_proj new_t old_t = let val (diff, stripped_t) = costrip_prodT new_t old_t val (tfrees, f_head) = map_comp_bnf stripped_t val f_args = map (K (Abs ("x", dummyT, Const (@{const_name undefined}, dummyT)))) tfrees fun add_snd 0 = list_comb (map_types (K dummyT) f_head, f_args) | add_snd n = Const (@{const_name comp}, dummyT) $ add_snd (n - 1) $ Const (@{const_name snd}, dummyT) in add_snd diff end fun construct_outer_proj new_t old_t = case (new_t, old_t) of (Type (@{type_name sum}, new_ts), Type (@{type_name sum}, old_ts)) => let val ps = map2 construct_outer_proj new_ts old_ts in list_comb (Const (@{const_name map_sum}, dummyT), ps) end | _ => construct_inner_proj new_t old_t val outer_proj = construct_outer_proj new_R_typ old_R_typ val old_R_typ_imported = yield_singleton Variable.importT_terms old_R ctxt |> fst |> get_typ val c = outer_proj |> Type.constraint (new_R_typ --> old_R_typ_imported) |> Syntax.check_term ctxt |> Thm.cterm_of ctxt val wf_simulate = Drule.infer_instantiate ctxt [(("g", 0), c)] @{thm wf_simulate_simple} val old_wf = (@{thm wfP_implies_wf_set_of} OF [@{thm accp_wfPI} OF [totality]]) val inner_tac = match_tac ctxt @{thms wf_implies_dom} THEN' match_tac ctxt [wf_simulate] CONTINUE_WITH_FW [resolve_tac ctxt [old_wf], match_tac ctxt @{thms set_ofI} THEN' dmatch_tac ctxt @{thms set_ofD} THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt [old_R_eq, new_R_eq]) THEN' TRY' (REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE exE}) THEN' hyp_subst_tac_thin true ctxt THEN' REPEAT_ALL_NEW (match_tac ctxt @{thms conjI exI}))] val unfold_tac = Local_Defs.unfold_tac ctxt @{thms comp_apply id_apply prod.sel} THEN auto_tac ctxt val tac = SOLVED (HEADGOAL inner_tac THEN unfold_tac) in if futile then (warning "Termination relation has sort constraints; termination proof is unlikely to be automatic or may even be impossible"; Seq.empty) else (tracing "Trying to re-use termination proof"; tac st) end) #> Exn.get_res #> the_default Seq.empty in simple_tac ORELSE smart_tac ORELSE fallback_tac true end | _ => fallback_tac false in SELECT_GOAL tac end end \ No newline at end of file diff --git a/thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy b/thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy --- a/thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy +++ b/thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy @@ -1,1203 +1,1203 @@ (****************************************************************************** * Isabelle/C * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) section \Interface: Inner and Outer Commands\ theory C_Command imports C_Eval keywords "C" :: thy_decl % "ML" and "C_file" :: thy_load % "ML" and "C_export_boot" :: thy_decl % "ML" and "C_export_file" :: thy_decl and "C_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) and "C_val" :: diag % "ML" begin subsection \Parsing Entry-Point: Error and Acceptance Cases\ ML \ \\<^file>\~~/src/Pure/Tools/ghc.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay Analogous to: (* Title: Pure/Tools/ghc.ML Author: Makarius Support for GHC: Glasgow Haskell Compiler. *)*) \ structure C_Serialize = struct (** string literals **) fun print_codepoint c = (case c of 10 => "\\n" | 9 => "\\t" | 11 => "\\v" | 8 => "\\b" | 13 => "\\r" | 12 => "\\f" | 7 => "\\a" | 27 => "\\e" | 92 => "\\\\" | 63 => "\\?" | 39 => "\\'" | 34 => "\\\"" | c => if c >= 32 andalso c < 127 then chr c else error "Not yet implemented"); fun print_symbol sym = (case Symbol.decode sym of Symbol.Char s => print_codepoint (ord s) | Symbol.UTF8 s => UTF8.decode_permissive s |> map print_codepoint |> implode | Symbol.Sym s => "\\092<" ^ s ^ ">" | Symbol.Control s => "\\092<^" ^ s ^ ">" | _ => translate_string (print_codepoint o ord) sym); val print_string = quote o implode o map print_symbol o Symbol.explode; end \ ML \ \\<^file>\~~/src/Pure/Tools/generated_files.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay Analogous to: (* Title: Pure/Tools/generated_files.ML Author: Makarius Generated source files for other languages: with antiquotations, without Isabelle symbols. *)*) \ structure C_Generated_Files = struct val c_dir = "C"; val c_ext = "c"; val c_make_comment = enclose "/*" "*/"; (** context data **) (* file types *) fun get_file_type ext = if ext = "" then error "Bad file extension" else if c_ext = ext then () else error ("Unknown file type for extension " ^ quote ext); (** Isar commands **) (* generate_file *) fun generate_file (binding, src_content) lthy = let val (path, pos) = Path.dest_binding binding; val () = get_file_type (#2 (Path.split_ext path)) handle ERROR msg => error (msg ^ Position.here pos); val header = c_make_comment " generated by Isabelle "; val content = header ^ "\n" ^ src_content; in lthy |> (Local_Theory.background_theory o Generated_Files.add_files) (binding, Bytes.string content) end; (** concrete file types **) val _ = Theory.setup (Generated_Files.file_type \<^binding>\C\ {ext = c_ext, make_comment = c_make_comment, make_string = C_Serialize.print_string}); end \ ML \ \\<^theory>\Isabelle_C.C_Eval\\ \ signature C_MODULE = sig structure Data_Accept : GENERIC_DATA structure Data_In_Env : GENERIC_DATA structure Data_In_Source : GENERIC_DATA structure Data_Term : GENERIC_DATA structure C_Term: sig val key0_default: string val key0_expression: string val key0_external_declaration: string val key0_statement: string val key0_translation_unit: string val key_default: Input.source val key_expression: Input.source val key_external_declaration: Input.source val key_statement: Input.source val key_translation_unit: Input.source val map_default: (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> local_theory -> term) -> theory -> theory val map_expression: (C_Grammar_Rule_Lib.CExpr -> C_Env.env_lang -> local_theory -> term) -> theory -> theory val map_external_declaration: (C_Grammar_Rule_Lib.CExtDecl -> C_Env.env_lang -> local_theory -> term) -> theory -> theory val map_statement: (C_Grammar_Rule_Lib.CStat -> C_Env.env_lang -> local_theory -> term) -> theory -> theory val map_translation_unit: (C_Grammar_Rule_Lib.CTranslUnit -> C_Env.env_lang -> local_theory -> term) -> theory -> theory val tok0_expression: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok0_external_declaration: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok0_statement: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok0_translation_unit: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok_expression: Input.source * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok_external_declaration: Input.source * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok_statement: Input.source * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok_translation_unit: Input.source * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tokens: (string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token)) list end structure C_Term': sig val accept: local_theory -> (Input.source * (Position.range -> (C_Grammar.Tokens.svalue, Position.T) LALR_Parser_Eval.Token.token)) option -> (Input.source -> Context.generic -> (C_Grammar.Tokens.svalue, Position.T) LALR_Parser_Eval.Token.token) * (Data_In_Env.T -> 'a * (C_Grammar_Rule.ast_generic * 'b * 'c) -> {context: Context.generic, error_lines: 'd, reports_text: 'e} -> term * {context: Context.generic, error_lines: 'd, reports_text: 'e}) val err: C_Env.env_lang -> (LALR_Table.state * (C_Grammar_Parser.svalue0 * Position.T * Position.T)) list -> Position.T -> {context: Context.generic, error_lines: string list, reports_text: Position.report_text list} -> term * {context: Context.generic, error_lines: string list, reports_text: Position.report_text list} val eval_in: Input.source -> Context.generic -> (Context.generic -> C_Env.env_lang) -> (Input.source * (Position.range -> (C_Grammar.Tokens.svalue, Position.T) LALR_Parser_Eval.Token.token)) option -> C_Lex.token list * (C_Env.error_lines -> string list) -> term val parse_translation: ('a * (Input.source * (Position.range -> (C_Grammar.Tokens.svalue, Position.T) LALR_Parser_Eval.Token.token)) option) list -> ('a * (Proof.context -> term list -> term)) list end val accept: Data_In_Env.T -> 'a * (C_Grammar_Rule.ast_generic * 'b * 'c) -> {context: Context.generic, error_lines: 'd, reports_text: 'e} -> unit * {context: Context.generic, error_lines: 'd, reports_text: 'e} val accept0: (Context.generic -> C_Grammar_Rule.ast_generic -> Data_In_Env.T -> Context.generic -> 'a) -> Data_In_Env.T -> C_Grammar_Rule.ast_generic -> Context.generic -> 'a val c_enclose: string -> string -> Input.source -> C_Lex.token list * (string list -> string list) val env: Context.generic -> Data_In_Env.T val env0: Proof.context -> Data_In_Env.T val err: C_Env.env_lang -> (LALR_Table.state * (C_Grammar_Parser.svalue0 * Position.T * Position.T)) list -> Position.T -> {context: Context.generic, error_lines: string list, reports_text: Position.report_text list} -> unit * {context: Context.generic, error_lines: string list, reports_text: Position.report_text list} val err0: 'a -> 'b -> Position.T -> {context: 'c, error_lines: string list, reports_text: 'd} -> {context: 'c, error_lines: string list, reports_text: 'd} val eval_in: Input.source -> Context.generic option -> C_Lex.token list * (C_Env.error_lines -> string list) -> unit val eval_source: Input.source -> unit val exec_eval: Input.source -> Context.generic -> Context.generic val start: Input.source -> Context.generic -> (C_Grammar.Tokens.svalue, Position.T) LALR_Parser_Eval.Token.token (* toplevel command semantics of Isabelle_C *) val C: Input.source -> Context.generic -> Context.generic val C': C_Env.env_lang option -> Input.source -> Context.generic -> Context.generic val C_export_boot: Input.source -> Context.generic -> generic_theory val C_export_file: Position.T * 'a -> Proof.context -> Proof.context val C_prf: Input.source -> Proof.state -> Proof.state end structure C_Module : C_MODULE = struct structure Data_In_Source = Generic_Data ( type T = Input.source list val empty = [] val merge = K empty ) structure Data_In_Env = Generic_Data ( type T = C_Env.env_lang val empty = C_Env.empty_env_lang val merge = K empty ) structure Data_Accept = Generic_Data ( type T = C_Grammar_Rule.ast_generic -> C_Env.env_lang -> Context.generic -> Context.generic fun empty _ _ = I val merge = #2 ) structure Data_Term = Generic_Data ( type T = (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> local_theory -> term) Symtab.table val empty = Symtab.empty val merge = #2 ) (* keys for major syntactic categories *) structure C_Term = struct val key_translation_unit = \translation_unit\ val key_external_declaration = \external_declaration\ val key_statement = \statement\ val key_expression = \expression\ val key_default = \default\ local val source_content = Input.source_content #> #1 in val key0_translation_unit = source_content key_translation_unit val key0_external_declaration = source_content key_external_declaration val key0_statement = source_content key_statement val key0_expression = source_content key_expression val key0_default = source_content key_default end val tok0_translation_unit = (key0_translation_unit, C_Grammar.Tokens.start_translation_unit) val tok0_external_declaration = ( key0_external_declaration , C_Grammar.Tokens.start_external_declaration) val tok0_statement = (key0_statement, C_Grammar.Tokens.start_statement) val tok0_expression = (key0_expression, C_Grammar.Tokens.start_expression) val tok_translation_unit = (key_translation_unit, C_Grammar.Tokens.start_translation_unit) val tok_external_declaration = ( key_external_declaration , C_Grammar.Tokens.start_external_declaration) val tok_statement = (key_statement, C_Grammar.Tokens.start_statement) val tok_expression = (key_expression, C_Grammar.Tokens.start_expression) val tokens = [ tok0_translation_unit , tok0_external_declaration , tok0_statement , tok0_expression ] local fun map_upd0 key v = Context.theory_map (Data_Term.map (Symtab.update (key, v))) fun map_upd key start f = map_upd0 key (f o the o start) in val map_translation_unit = map_upd key0_translation_unit C_Grammar_Rule.get_CTranslUnit val map_external_declaration = map_upd key0_external_declaration C_Grammar_Rule.get_CExtDecl val map_statement = map_upd key0_statement C_Grammar_Rule.get_CStat val map_expression = map_upd key0_expression C_Grammar_Rule.get_CExpr val map_default = map_upd0 key0_default end end fun env0 ctxt = case Config.get ctxt C_Options.starting_env of "last" => Data_In_Env.get (Context.Proof ctxt) | "empty" => C_Env.empty_env_lang | s => error ("Unknown option: " ^ s ^ Position.here (Config.pos_of C_Options.starting_env)) val env = env0 o Context.proof_of fun start source context = Input.range_of source |> let val s = Config.get (Context.proof_of context) C_Options.starting_rule in case AList.lookup (op =) C_Term.tokens s of SOME tok => tok | NONE => error ("Unknown option: " ^ s ^ Position.here (Config.pos_of C_Options.starting_rule)) end fun err0 _ _ pos = C_Env.map_error_lines (cons ("Parser: No matching grammar rule" ^ Position.here pos)) val err = pair () oooo err0 fun accept0 f env_lang ast = Data_In_Env.put env_lang #> (fn context => f context ast env_lang (Data_Accept.get context ast env_lang context)) fun accept env_lang (_, (ast, _, _)) = pair () o C_Env.map_context (accept0 (K (K (K I))) env_lang ast) val eval_source = C_Context.eval_source env start err accept fun c_enclose bg en source = C_Lex.@@ ( C_Lex.@@ (C_Lex.read bg, C_Lex.read_source source) , C_Lex.read en); structure C_Term' = struct val err = pair Term.dummy oooo err0 fun accept ctxt start_rule = let val (key, start) = case start_rule of NONE => (C_Term.key_default, start) | SOME (key, start_rule) => (key, fn source => fn _ => start_rule (Input.range_of source)) val (key, pos) = Input.source_content key in ( start , fn env_lang => fn (_, (ast, _, _)) => C_Env.map_context' (accept0 (fn context => pair oo (case Symtab.lookup (Data_Term.get context) key of NONE => tap (fn _ => warning ("Representation function associated to\ \ \"" ^ key ^ "\"" ^ Position.here pos ^ " not found (returning a dummy term)")) (fn _ => fn _ => @{term "()"}) | SOME f => fn ast => fn env_lang => f ast env_lang ctxt)) env_lang ast)) end fun eval_in text context env start_rule = let val (start, accept) = accept (Context.proof_of context) start_rule in C_Context.eval_in (SOME context) env (start text) err accept end fun parse_translation l = l |> map (apsnd (fn start_rule => fn ctxt => fn args => let val msg = (case start_rule of NONE => C_Term.key_default | SOME (key, _) => key) |> Input.source_content |> #1 fun err () = raise TERM (msg, args) in case args of [(c as Const (\<^syntax_const>\_constrain\, _)) $ Free (s, _) $ p] => (case Term_Position.decode_position p of SOME (pos, _) => c $ let val src = uncurry (Input.source false) let val s0 = Symbol_Pos.explode (s, pos) val s = Symbol_Pos.cartouche_content s0 in ( Symbol_Pos.implode s , case s of [] => Position.no_range | (_, pos0) :: _ => Position.range (pos0, s0 |> List.last |> snd)) end in eval_in src (case Context.get_generic_context () of NONE => Context.Proof ctxt | SOME context => Context.mapping I (K ctxt) context) (C_Stack.Data_Lang.get #> (fn NONE => env0 ctxt | SOME (_, env_lang) => env_lang)) start_rule (c_enclose "" "" src) end $ p | NONE => err ()) | _ => err () end)) end fun eval_in text ctxt = C_Context.eval_in ctxt env (start text) err accept fun exec_eval source = Data_In_Source.map (cons source) #> ML_Context.exec (fn () => eval_source source) fun C_prf source = Proof.map_context (Context.proof_map (exec_eval source)) #> Proof.propagate_ml_env fun C_export_boot source context = context |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle |> Config.put_generic ML_Env.ML_write_global true |> exec_eval source |> Config.restore_generic ML_Env.ML_write_global context |> Config.restore_generic ML_Env.ML_environment context |> Local_Theory.propagate_ml_env fun C source = exec_eval source #> Local_Theory.propagate_ml_env val C' = let fun C env_lang src context = context |> C_Env.empty_env_tree |> C_Context.eval_source' env_lang (fn src => start src context) err accept src |> (fn (_, {context, reports_text, error_lines}) => tap (fn _ => case error_lines of [] => () | l => warning (cat_lines (rev l))) (C_Stack.Data_Tree.map (curry C_Stack.Data_Tree_Args.merge (reports_text, [])) context)) in fn NONE => (fn src => C (env (Context.the_generic_context ())) src) | SOME env_lang => C env_lang end fun C_export_file (pos, _) lthy = let val c_sources = Data_In_Source.get (Context.Proof lthy) val binding = Path.binding ( Path.appends [ Path.basic C_Generated_Files.c_dir , Path.basic (string_of_int (length c_sources)) , lthy |> Proof_Context.theory_of |> Context.theory_base_name |> Path.explode |> Path.ext C_Generated_Files.c_ext ] , pos) in lthy |> C_Generated_Files.generate_file (binding, rev c_sources |> map (Input.source_content #> #1) |> cat_lines) |> tap (Proof_Context.theory_of #> (fn thy => let val file = Generated_Files.get_file thy binding in Generated_Files.export_file thy file; writeln (Export.message thy Path.current); writeln (prefix " " (Generated_Files.print_file file)) end)) end end \ subsection \Definitions of C11 Directives as C-commands\ subsubsection \Initialization\ ML \ \\<^theory>\Pure\\ \ structure C_Directive : sig val setup_define: Position.T -> (C_Lex.token list -> string * Position.range -> Context.generic -> C_Lex.token list * Context.generic) -> (string * Position.range -> Context.generic -> Context.generic) -> theory -> theory end = struct local fun directive_update keyword data = C_Context.directive_update keyword (data, K (K (K I))) fun return f (env_cond, env) = ([], (env_cond, f env)) fun directive_update_define pos f_toks f_antiq = directive_update ("define", pos) (return o (fn C_Lex.Define (_, C_Lex.Group1 ([], [tok3]), NONE, C_Lex.Group1 ([], toks)) => let val map_ctxt = case (tok3, toks) of (C_Lex.Token ((pos, _), (C_Lex.Ident _, ident)), [C_Lex.Token (_, (C_Lex.Integer (_, C_Lex.Repr_decimal, []), integer))]) => C_Env.map_context (Context.map_theory (Named_Target.theory_map (Specification.definition_cmd (SOME (Binding.make (ident, pos), NONE, NoSyn)) [] [] (Binding.empty_atts, ident ^ " \ " ^ integer) true #> tap (fn ((_, (_, t)), ctxt) => Output.information ("Generating " ^ Pretty.string_of (Syntax.pretty_term ctxt (Thm.prop_of t)) ^ Position.here (Position.range_position ( C_Lex.pos_of tok3 , C_Lex.end_pos_of (List.last toks))))) #> #2))) | _ => I in fn (env_dir, env_tree) => let val name = C_Lex.content_of tok3 val pos = [C_Lex.pos_of tok3] val data = (pos, serial (), (C_Scan.Left (f_toks toks), f_antiq)) in ( Symtab.update (name, data) env_dir , env_tree |> C_Context.markup_directive_define false (C_Ast.Left (data, C_Env_Ext.list_lookup env_dir name)) pos name |> map_ctxt) end end | C_Lex.Define (_, C_Lex.Group1 ([], [tok3]), SOME (C_Lex.Group1 (_ :: toks_bl, _)), _) => tap (fn _ => (* not yet implemented *) warning ("Ignored functional macro directive" ^ Position.here (Position.range_position (C_Lex.pos_of tok3, C_Lex.end_pos_of (List.last toks_bl))))) | _ => I)) in val setup_define = Context.theory_map o C_Context0.Directives.map ooo directive_update_define val _ = Theory.setup (Context.theory_map (C_Context0.Directives.map (directive_update_define \<^here> (K o pair) (K I) #> directive_update ("undef", \<^here>) (return o (fn C_Lex.Undef (C_Lex.Group2 (_, _, [tok])) => (fn (env_dir, env_tree) => let val name = C_Lex.content_of tok val pos1 = [C_Lex.pos_of tok] val data = Symtab.lookup env_dir name in ( (case data of NONE => env_dir | SOME _ => Symtab.delete name env_dir) , C_Context.markup_directive_define true (C_Ast.Right (pos1, data)) pos1 name env_tree) end) | _ => I))))) end end \ subsection \Definitions of C Annotation Commands\ subsubsection \Library\ ML \ \\<^file>\~~/src/Pure/Isar/toplevel.ML\\ \ structure C_Inner_Toplevel = struct val theory = Context.map_theory fun local_theory' target f gthy = let val (finish, lthy) = Target_Context.switch_named_cmd target gthy; val lthy' = lthy |> Local_Theory.new_group |> f false |> Local_Theory.reset_group; in finish lthy' end val generic_theory = I fun keep'' f = tap (f o Context.proof_of) end \ ML \ \\<^file>\~~/src/Pure/Isar/isar_cmd.ML\\ \ structure C_Inner_Isar_Cmd = struct (** theory declarations **) (* generic setup *) fun setup0 f_typ f_val src = fn NONE => let val setup = "setup" in C_Context.expression "C_Ast" (Input.range_of src) setup (f_typ "C_Stack.stack_data" "C_Stack.stack_data_elem -> C_Env.env_lang -> Context.generic -> Context.generic") ("fn context => \ \let val (stack, env_lang) = C_Stack.Data_Lang.get' context \ \in " ^ f_val setup "stack" ^ " (stack |> hd) env_lang end context") (ML_Lex.read_source src) end | SOME rule => let val hook = "hook" in C_Context.expression "C_Ast" (Input.range_of src) hook (f_typ "C_Stack.stack_data" (C_Grammar_Rule.type_reduce rule ^ " C_Stack.stack_elem -> C_Env.env_lang -> Context.generic -> Context.generic")) ("fn context => \ \let val (stack, env_lang) = C_Stack.Data_Lang.get' context \ \in " ^ f_val hook "stack" ^ " " ^ "(stack \ \|> hd \ \|> C_Stack.map_svalue0 C_Grammar_Rule.reduce" ^ Int.toString rule ^ ")\ \env_lang \ \end \ \ context") (ML_Lex.read_source src) end val setup = setup0 (fn a => fn b => a ^ " -> " ^ b) (fn a => fn b => a ^ " " ^ b) val setup' = setup0 (K I) K (* print theorems, terms, types etc. *) local fun string_of_term ctxt s = let val t = Syntax.read_term ctxt s; val T = Term.type_of t; val ctxt' = Proof_Context.augment t ctxt; in Pretty.string_of (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk, Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]) end; fun print_item string_of (modes, arg) ctxt = Print_Mode.with_modes modes (fn () => writeln (string_of ctxt arg)) (); in val print_term = print_item string_of_term; end; end \ ML \ \\<^file>\~~/src/Pure/Isar/outer_syntax.ML\\ \ structure C_Inner_Syntax = struct val drop1 = fn C_Scan.Left f => C_Scan.Left (K o f) | C_Scan.Right (f, dir) => C_Scan.Right (K o f, dir) val drop2 = fn C_Scan.Left f => C_Scan.Left (K o K o f) | C_Scan.Right (f, dir) => C_Scan.Right (K o K o f, dir) val bottom_up = C_Env.Bottom_up o C_Env.Exec_annotation (**) fun pref_lex name = "#" ^ name val pref_bot = I fun pref_top name = name ^ "\" (**) fun command2' cmd f (pos_bot, pos_top) = let fun cmd' dir = cmd (C_Scan.Right (f, dir)) Keyword.thy_decl in cmd' bottom_up (pref_bot, pos_bot) #> cmd' C_Env.Top_down (pref_top, pos_top) end fun command3' cmd f (pos_lex, pos_bot, pos_top) = cmd (C_Scan.Left f) (pref_lex, pos_lex) #> command2' (K o cmd) f (pos_bot, pos_top) fun command2 cmd f (name, pos_bot, pos_top) = command2' (fn f => fn kind => fn (name_pref, pos) => cmd f kind (name_pref name, pos)) f (pos_bot, pos_top) fun command3 cmd f (name, pos_lex, pos_bot, pos_top) = command3' (fn f => fn (name_pref, pos) => cmd f (name_pref name, pos)) f (pos_lex, pos_bot, pos_top) (**) fun command00 f kind scan name = C_Annotation.command'' kind name "" (case f of C_Scan.Left f => (fn _ => C_Parse.range scan >> (fn (src, range) => C_Env.Lexing (range, f src range))) | C_Scan.Right (f, dir) => fn ((stack1, (to_delay, stack2)), _) => C_Parse.range scan >> (fn (src, range) => C_Env.Parsing ((stack1, stack2), (range, dir (f src range), Symtab.empty, to_delay)))) fun command00_no_range f kind name = C_Annotation.command'' kind name "" (case f of C_Scan.Left f => (fn (_, range) => Scan.succeed () >> K (C_Env.Lexing (range, f range))) | C_Scan.Right (f, dir) => fn ((stack1, (to_delay, stack2)), range) => Scan.succeed () >> K (C_Env.Parsing ((stack1, stack2), (range, dir (f range), Symtab.empty, to_delay)))) (**) fun command' f = command00 (drop1 f) Keyword.thy_decl fun command f scan = command2 (fn f => fn kind => command00 f kind scan) (K o f) fun command_range f = command00_no_range f Keyword.thy_decl val command_range' = command3 (command_range o drop1) fun command_no_range' f = command00_no_range (drop1 f) Keyword.thy_decl fun command_no_range f = command2 command00_no_range (K f) fun command0 f scan = command3 (fn f => command' (drop1 f) scan) f fun local_command' (name, pos_lex, pos_bot, pos_top) scan f = command3' (fn f => fn (name_pref, pos) => command' (drop1 f) (C_Token.syntax' (Parse.opt_target -- scan name_pref)) (name_pref name, pos)) (fn (target, arg) => C_Inner_Toplevel.local_theory' target (f arg)) (pos_lex, pos_bot, pos_top) fun local_command'' spec = local_command' spec o K val command0_no_range = command_no_range' o drop1 fun command0' f kind scan = command3 (fn f => command00 (drop2 f) kind scan) f end \ ML \ \\<^file>\~~/src/Pure/ML/ml_file.ML\\ \ structure C_Inner_File = struct fun command_c ({lines, pos, ...}: Token.file) = C_Module.C (Input.source true (cat_lines lines) (pos, pos)); fun C get_file gthy = command_c (get_file (Context.theory_of gthy)) gthy; -fun command_ml environment debug get_file gthy = +fun command_ml environment catch_all debug get_file gthy = let val file = get_file (Context.theory_of gthy); val source = Token.file_source file; val _ = Document_Output.check_comments (Context.proof_of gthy) (Input.source_explode source); val flags: ML_Compiler.flags = - {environment = environment, redirect = true, verbose = true, + {environment = environment, redirect = true, verbose = true, catch_all = catch_all, debug = debug, writeln = writeln, warning = warning}; in gthy |> ML_Context.exec (fn () => ML_Context.eval_source flags source) |> Local_Theory.propagate_ml_env end; -val ML = command_ml ""; -val SML = command_ml ML_Env.SML; +val ML = command_ml "" false; +val SML = command_ml ML_Env.SML true; end; \ subsubsection \Initialization\ setup \ \\<^theory>\Pure\\ \ C_Thy_Header.add_keywords_minor (maps (fn ((name, pos_lex, pos_bot, pos_top), ty) => [ ((C_Inner_Syntax.pref_lex name, pos_lex), ty) , ((C_Inner_Syntax.pref_bot name, pos_bot), ty) , ((C_Inner_Syntax.pref_top name, pos_top), ty) ]) [ (("apply", \<^here>, \<^here>, \<^here>), Keyword.command_spec (Keyword.prf_script, ["proof"])) , (("by", \<^here>, \<^here>, \<^here>), Keyword.command_spec (Keyword.qed, ["proof"])) , (("done", \<^here>, \<^here>, \<^here>), Keyword.command_spec (Keyword.qed_script, ["proof"])) ]) \ ML \ \\<^theory>\Pure\\ \ local val semi = Scan.option (C_Parse.$$$ ";"); structure C_Isar_Cmd = struct fun ML source = ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #> Local_Theory.propagate_ml_env fun theorem schematic ((long, binding, includes, elems, concl), (l_meth, o_meth)) int lthy = (if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) long Thm.theoremK NONE (K I) binding includes elems concl int lthy |> fold (fn m => tap (fn _ => Method.report m) #> Proof.apply m #> Seq.the_result "") l_meth |> (case o_meth of NONE => Proof.global_done_proof | SOME (m1, m2) => tap (fn _ => (Method.report m1; Option.map Method.report m2)) #> Proof.global_terminal_proof (m1, m2)) fun definition (((decl, spec), prems), params) = #2 oo Specification.definition_cmd decl params prems spec fun declare (facts, fixes) = #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes end local val long_keyword = Parse_Spec.includes >> K "" || Parse_Spec.long_statement_keyword; val long_statement = Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts -- Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl)); val short_statement = Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows)); in fun theorem spec schematic = C_Inner_Syntax.local_command' spec (fn name_pref => (long_statement || short_statement) -- let val apply = Parse.$$$ (name_pref "apply") |-- Method.parse in Scan.repeat1 apply -- (Parse.$$$ (name_pref "done") >> K NONE) || Scan.repeat apply -- (Parse.$$$ (name_pref "by") |-- Method.parse -- Scan.option Method.parse >> SOME) end) (C_Isar_Cmd.theorem schematic) end val opt_modes = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\)\)) []; val _ = Theory.setup ( C_Inner_Syntax.command (C_Inner_Toplevel.generic_theory oo C_Inner_Isar_Cmd.setup) C_Parse.ML_source ("\setup", \<^here>, \<^here>) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.theory o Isar_Cmd.setup) C_Parse.ML_source ("setup", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.generic_theory o C_Isar_Cmd.ML) C_Parse.ML_source ("ML", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.generic_theory o C_Module.C) C_Parse.C_source ("C", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0' (C_Inner_Toplevel.generic_theory o C_Inner_File.ML NONE) Keyword.thy_load (C_Resources.parse_file --| semi) ("ML_file", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0' (C_Inner_Toplevel.generic_theory o C_Inner_File.C) Keyword.thy_load (C_Resources.parse_file --| semi) ("C_file", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.generic_theory o C_Module.C_export_boot) C_Parse.C_source ("C_export_boot", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command_range' (Context.map_theory o Named_Target.theory_map o C_Module.C_export_file) ("C_export_file", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command_no_range (C_Inner_Toplevel.generic_theory oo C_Inner_Isar_Cmd.setup \fn ((_, (_, pos1, pos2)) :: _) => (fn _ => fn _ => tap (fn _ => Position.reports_text [((Position.range (pos1, pos2) |> Position.range_position, Markup.intensify), "")])) | _ => fn _ => fn _ => I\) ("highlight", \<^here>, \<^here>) #> theorem ("theorem", \<^here>, \<^here>, \<^here>) false #> theorem ("lemma", \<^here>, \<^here>, \<^here>) false #> theorem ("corollary", \<^here>, \<^here>, \<^here>) false #> theorem ("proposition", \<^here>, \<^here>, \<^here>) false #> theorem ("schematic_goal", \<^here>, \<^here>, \<^here>) true #> C_Inner_Syntax.local_command'' ("definition", \<^here>, \<^here>, \<^here>) (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes) C_Isar_Cmd.definition #> C_Inner_Syntax.local_command'' ("declare", \<^here>, \<^here>, \<^here>) (Parse.and_list1 Parse.thms1 -- Parse.for_fixes) C_Isar_Cmd.declare #> C_Inner_Syntax.command0 (C_Inner_Toplevel.keep'' o C_Inner_Isar_Cmd.print_term) (C_Token.syntax' (opt_modes -- Parse.term)) ("term", \<^here>, \<^here>, \<^here>)) in end \ subsection \Definitions of Outer Classical Commands\ subsubsection \Library\ (* Author: Frédéric Tuong, Université Paris-Saclay Analogous to: (* Title: Pure/Pure.thy Author: Makarius The Pure theory, with definitions of Isar commands and some lemmas. *)*) ML \ \\<^file>\~~/src/Pure/Isar/parse.ML\\ \ structure C_Outer_Parse = struct val C_source = Parse.input (Parse.group (fn () => "C source") Parse.embedded) end \ ML \ \\<^file>\~~/src/Pure/Isar/outer_syntax.ML\\ \ structure C_Outer_Syntax = struct val _ = Outer_Syntax.command \<^command_keyword>\C\ "" (C_Outer_Parse.C_source >> (Toplevel.generic_theory o C_Module.C)); end \ ML \ \\<^file>\~~/src/Pure/Isar/isar_cmd.ML\\ \ structure C_Outer_Isar_Cmd = struct (* diagnostic ML evaluation *) structure Diag_State = Proof_Data ( type T = Toplevel.state option; fun init _ = NONE; ); fun C_diag source state = let val opt_ctxt = try Toplevel.generic_theory_of state |> Option.map (Context.proof_of #> Diag_State.put (SOME state)); in Context.setmp_generic_context (Option.map Context.Proof opt_ctxt) (fn () => C_Module.eval_source source) () end; fun diag_state ctxt = (case Diag_State.get ctxt of SOME st => st | NONE => Toplevel.make_state NONE); val diag_goal = Proof.goal o Toplevel.proof_of o diag_state; val _ = Theory.setup (ML_Antiquotation.value (Binding.qualify true "Isar" \<^binding>\C_state\) (Scan.succeed "C_Outer_Isar_Cmd.diag_state ML_context") #> ML_Antiquotation.value (Binding.qualify true "Isar" \<^binding>\C_goal\) (Scan.succeed "C_Outer_Isar_Cmd.diag_goal ML_context")); end \ ML \ \\<^file>\~~/src/Pure/ML/ml_file.ML\\ \ structure C_Outer_File = struct fun command_c ({src_path, lines, digest, pos}: Token.file) = let val provide = Resources.provide (src_path, digest); in I #> C_Module.C (Input.source true (cat_lines lines) (pos, pos)) #> Context.mapping provide (Local_Theory.background_theory provide) end; fun C get_file gthy = command_c (get_file (Context.theory_of gthy)) gthy; end; \ subsubsection \Setup for \<^verbatim>\C\ and \<^verbatim>\C_file\ Command Syntax\ ML \ \\<^theory>\Pure\\ \ local val semi = Scan.option \<^keyword>\;\; val _ = Outer_Syntax.command \<^command_keyword>\C_file\ "read and evaluate Isabelle/C file" (Resources.parse_file --| semi >> (Toplevel.generic_theory o C_Outer_File.C)); val _ = Outer_Syntax.command \<^command_keyword>\C_export_boot\ "C text within theory or local theory, and export to bootstrap environment" (C_Outer_Parse.C_source >> (Toplevel.generic_theory o C_Module.C_export_boot)); val _ = Outer_Syntax.command \<^command_keyword>\C_prf\ "C text within proof" (C_Outer_Parse.C_source >> (Toplevel.proof o C_Module.C_prf)); val _ = Outer_Syntax.command \<^command_keyword>\C_val\ "diagnostic C text" (C_Outer_Parse.C_source >> (Toplevel.keep o C_Outer_Isar_Cmd.C_diag)); val _ = Outer_Syntax.local_theory \<^command_keyword>\C_export_file\ "diagnostic C text" (Scan.succeed () >> K (C_Module.C_export_file Position.no_range)); in end\ subsection \Term-Cartouches for C Syntax\ syntax "_C_translation_unit" :: \cartouche_position \ string\ ("\<^C>\<^sub>u\<^sub>n\<^sub>i\<^sub>t _") syntax "_C_external_declaration" :: \cartouche_position \ string\ ("\<^C>\<^sub>d\<^sub>e\<^sub>c\<^sub>l _") syntax "_C_expression" :: \cartouche_position \ string\ ("\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r _") syntax "_C_statement" :: \cartouche_position \ string\ ("\<^C>\<^sub>s\<^sub>t\<^sub>m\<^sub>t _") syntax "_C" :: \cartouche_position \ string\ ("\<^C> _") parse_translation \ C_Module.C_Term'.parse_translation [ (\<^syntax_const>\_C_translation_unit\, SOME C_Module.C_Term.tok_translation_unit) , (\<^syntax_const>\_C_external_declaration\, SOME C_Module.C_Term.tok_external_declaration) , (\<^syntax_const>\_C_expression\, SOME C_Module.C_Term.tok_expression) , (\<^syntax_const>\_C_statement\, SOME C_Module.C_Term.tok_statement) , (\<^syntax_const>\_C\, NONE) ] \ (*test*) ML\C_Module.env (Context.the_generic_context())\ ML\open Args\ subsection\C-env related ML-Antiquotations as Programming Support\ ML\ (* was in Isabelle2020: (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => with: val embedded_token = ident || string || cartouche; val embedded_inner_syntax = embedded_token >> Token.inner_syntax_of; val embedded_input = embedded_token >> Token.input_of; val embedded = embedded_token >> Token.content_of; val embedded_position = embedded_input >> Input.source_content; defined in args. Setting it to : (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, (name, pos)) => makes this syntactically more restrictive. *) val _ = Theory.setup( ML_Antiquotation.value_embedded \<^binding>\C\<^sub>e\<^sub>n\<^sub>v\ (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, (name, pos)) => (warning"arg variant not implemented";"C_Module.env (Context.the_generic_context())")) || Scan.succeed "C_Module.env (Context.the_generic_context())")) \ text\Note that this anti-quotation is controlled by the \<^verbatim>\C_starting_env\ - flag. \ declare[[C\<^sub>e\<^sub>n\<^sub>v\<^sub>0 = last]] ML\@{C\<^sub>e\<^sub>n\<^sub>v}\ declare[[C\<^sub>e\<^sub>n\<^sub>v\<^sub>0 = empty]] ML\@{C\<^sub>e\<^sub>n\<^sub>v}\ subsection\The Standard Store C11-AST's generated from C-commands\ text\Each call of the C command will register the parsed root AST in this theory-name indexed table.\ ML\ structure Root_Ast_Store = Generic_Data (type T = C_Grammar_Rule.ast_generic list Symtab.table val empty = Symtab.empty val merge = K empty); Root_Ast_Store.map: ( C_Grammar_Rule.ast_generic list Symtab.table -> C_Grammar_Rule.ast_generic list Symtab.table) -> Context.generic -> Context.generic; fun update_Root_Ast filter ast _ ctxt = let val theory_id = Context.theory_long_name(Context.theory_of ctxt) val insert_K_ast = Symtab.map_default (theory_id,[]) (cons ast) in case filter ast of NONE => (warning "No appropriate c11 ast found - store unchanged."; ctxt) |SOME _ => (Root_Ast_Store.map insert_K_ast) ctxt end; fun get_Root_Ast filter thy = let val ctxt = Context.Theory thy val thid = Context.theory_long_name(Context.theory_of ctxt) val ast = case Symtab.lookup (Root_Ast_Store.get ctxt) (thid) of SOME (a::_) => (case filter a of NONE => error "Last C command is not of appropriate AST-class." | SOME x => x) | _ => error"No C command in the current theory." in ast end val get_CExpr = get_Root_Ast C_Grammar_Rule.get_CExpr; val get_CStat = get_Root_Ast C_Grammar_Rule.get_CStat; val get_CExtDecl = get_Root_Ast C_Grammar_Rule.get_CExtDecl; val get_CTranslUnit = get_Root_Ast C_Grammar_Rule.get_CTranslUnit; \ setup \Context.theory_map (C_Module.Data_Accept.put (update_Root_Ast SOME))\ ML\ (* Was : Args.embedded_position changed to : Args.name_position. See comment above. *) val _ = Theory.setup( ML_Antiquotation.value_embedded \<^binding>\C11_CTranslUnit\ (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, (name, pos)) => (warning"arg variant not implemented";"get_CTranslUnit (Context.the_global_context())")) || Scan.succeed "get_CTranslUnit (Context.the_global_context())") #> ML_Antiquotation.value_embedded \<^binding>\C11_CExtDecl\ (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, (name, pos)) => (warning"arg variant not implemented";"get_CExtDecl (Context.the_global_context())")) || Scan.succeed "get_CExtDecl (Context.the_global_context())") #> ML_Antiquotation.value_embedded \<^binding>\C11_CStat\ (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, (name, pos)) => (warning"arg variant not implemented";"get_CStat (Context.the_global_context())")) || Scan.succeed "get_CStat (Context.the_global_context())") #> ML_Antiquotation.value_embedded \<^binding>\C11_CExpr\ (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, (name, pos)) => (warning"arg variant not implemented";"get_CExpr (Context.the_global_context())")) || Scan.succeed "get_CExpr (Context.the_global_context())") ) \ end diff --git a/thys/Isabelle_Meta_Model/meta_isabelle/Printer_init.thy b/thys/Isabelle_Meta_Model/meta_isabelle/Printer_init.thy --- a/thys/Isabelle_Meta_Model/meta_isabelle/Printer_init.thy +++ b/thys/Isabelle_Meta_Model/meta_isabelle/Printer_init.thy @@ -1,438 +1,438 @@ (****************************************************************************** * Citadelle * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France * 2013-2017 IRT SystemX, France * 2011-2015 Achim D. Brucker, Germany * 2016-2018 The University of Sheffield, UK * 2016-2017 Nanyang Technological University, Singapore * 2017-2018 Virginia Tech, USA * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) section\Initializing the Printer\ theory Printer_init imports "../Init" "../isabelle_home/src/HOL/Isabelle_Main1" begin text\At the time of writing, the following target languages supported by Isabelle are also supported by the meta-compiler: Haskell, OCaml, Scala, SML.\ subsection\Kernel Code for Target Languages\ (* We put in 'CodeConst' functions using characters not allowed in a Isabelle 'code_const' expr (e.g. '_', '"', ...) *) lazy_code_printing code_module "CodeType" \ (Haskell) \ module CodeType where { type MlInt = Integer ; type MlMonad a = IO a }\ | code_module "CodeConst" \ (Haskell) \ module CodeConst where { import System.Directory ; import System.IO ; import qualified CodeConst.Printf ; outFile1 f file = (do fileExists <- doesFileExist file if fileExists then error ("File exists " ++ file ++ "\n") else do h <- openFile file WriteMode f (\pat -> hPutStr h . CodeConst.Printf.sprintf1 pat) hClose h) ; outStand1 :: ((String -> String -> IO ()) -> IO ()) -> IO () ; outStand1 f = f (\pat -> putStr . CodeConst.Printf.sprintf1 pat) }\ | code_module "CodeConst.Monad" \ (Haskell) \ module CodeConst.Monad where { bind a = (>>=) a ; return :: a -> IO a ; return = Prelude.return }\ | code_module "CodeConst.Printf" \ (Haskell) \ module CodeConst.Printf where { import Text.Printf ; sprintf0 = id ; sprintf1 :: PrintfArg a => String -> a -> String ; sprintf1 = printf ; sprintf2 :: PrintfArg a => PrintfArg b => String -> a -> b -> String ; sprintf2 = printf ; sprintf3 :: PrintfArg a => PrintfArg b => PrintfArg c => String -> a -> b -> c -> String ; sprintf3 = printf ; sprintf4 :: PrintfArg a => PrintfArg b => PrintfArg c => PrintfArg d => String -> a -> b -> c -> d -> String ; sprintf4 = printf ; sprintf5 :: PrintfArg a => PrintfArg b => PrintfArg c => PrintfArg d => PrintfArg e => String -> a -> b -> c -> d -> e -> String ; sprintf5 = printf }\ | code_module "CodeConst.String" \ (Haskell) \ module CodeConst.String where { concat s [] = [] ; concat s (x : xs) = x ++ concatMap ((++) s) xs }\ | code_module "CodeConst.Sys" \ (Haskell) \ module CodeConst.Sys where { import System.Directory ; isDirectory2 = doesDirectoryExist }\ | code_module "CodeConst.To" \ (Haskell) \ module CodeConst.To where { nat = id }\ | code_module "" \ (OCaml) \ module CodeType = struct type mlInt = int type 'a mlMonad = 'a option end module CodeConst = struct let outFile1 f file = try let () = if Sys.file_exists file then Printf.eprintf "File exists \"%S\"\n" file else () in let oc = open_out file in let b = f (fun s a -> try Some (Printf.fprintf oc s a) with _ -> None) in let () = close_out oc in b with _ -> None let outStand1 f = f (fun s a -> try Some (Printf.fprintf stdout s a) with _ -> None) module Monad = struct let bind = function None -> fun _ -> None | Some a -> fun f -> f a let return a = Some a end module Printf = struct include Printf let sprintf0 = sprintf let sprintf1 = sprintf let sprintf2 = sprintf let sprintf3 = sprintf let sprintf4 = sprintf let sprintf5 = sprintf end module String = String module Sys = struct open Sys let isDirectory2 s = try Some (is_directory s) with _ -> None end module To = struct let nat big_int x = Big_int.int_of_big_int (big_int x) end end \ | code_module "" \ (Scala) \ object CodeType { type mlMonad [A] = Option [A] type mlInt = Int } object CodeConst { def outFile1 [A] (f : (String => A => Option [Unit]) => Option [Unit], file0 : String) : Option [Unit] = { val file = new java.io.File (file0) if (file .isFile) { None } else { val writer = new java.io.PrintWriter (file) f ((fmt : String) => (s : A) => Some (writer .write (fmt .format (s)))) Some (writer .close ()) } } def outStand1 [A] (f : (String => A => Option [Unit]) => Option [Unit]) : Option[Unit] = { f ((fmt : String) => (s : A) => Some (print (fmt .format (s)))) } object Monad { def bind [A, B] (x : Option [A], f : A => Option [B]) : Option [B] = x match { case None => None case Some (a) => f (a) } def Return [A] (a : A) = Some (a) } object Printf { def sprintf0 (x0 : String) = x0 def sprintf1 [A1] (fmt : String, x1 : A1) = fmt .format (x1) def sprintf2 [A1, A2] (fmt : String, x1 : A1, x2 : A2) = fmt .format (x1, x2) def sprintf3 [A1, A2, A3] (fmt : String, x1 : A1, x2 : A2, x3 : A3) = fmt .format (x1, x2, x3) def sprintf4 [A1, A2, A3, A4] (fmt : String, x1 : A1, x2 : A2, x3 : A3, x4 : A4) = fmt .format (x1, x2, x3, x4) def sprintf5 [A1, A2, A3, A4, A5] (fmt : String, x1 : A1, x2 : A2, x3 : A3, x4 : A4, x5 : A5) = fmt .format (x1, x2, x3, x4, x5) } object String { def concat (s : String, l : List [String]) = l filter (_ .nonEmpty) mkString s } object Sys { def isDirectory2 (s : String) = Some (new java.io.File (s) .isDirectory) } object To { def nat [A] (f : A => BigInt, x : A) = f (x) .intValue () } } \ | code_module "" \ (SML) \ structure CodeType = struct type mlInt = string type 'a mlMonad = 'a option end structure CodeConst = struct structure Monad = struct val bind = fn NONE => (fn _ => NONE) | SOME a => fn f => f a val return = SOME end structure Printf = struct local fun sprintf s l = case String.fields (fn #"%" => true | _ => false) s of [] => "" | [x] => x | x :: xs => let fun aux acc l_pat l_s = case l_pat of [] => rev acc | x :: xs => aux (String.extract (x, 1, NONE) :: hd l_s :: acc) xs (tl l_s) in String.concat (x :: aux [] xs l) end in fun sprintf0 s_pat = s_pat fun sprintf1 s_pat s1 = sprintf s_pat [s1] fun sprintf2 s_pat s1 s2 = sprintf s_pat [s1, s2] fun sprintf3 s_pat s1 s2 s3 = sprintf s_pat [s1, s2, s3] fun sprintf4 s_pat s1 s2 s3 s4 = sprintf s_pat [s1, s2, s3, s4] fun sprintf5 s_pat s1 s2 s3 s4 s5 = sprintf s_pat [s1, s2, s3, s4, s5] end end structure String = struct val concat = String.concatWith end structure Sys = struct val isDirectory2 = SOME o File.is_dir o Path.explode handle ERROR _ => K NONE end structure To = struct fun nat f = Int.toString o f end fun outFile1 f file = let val pfile = Path.explode file val () = if File.exists pfile then error ("File exists \"" ^ file ^ "\"\n") else () val oc = Unsynchronized.ref [] val _ = f (fn a => fn b => SOME (oc := Printf.sprintf1 a b :: (Unsynchronized.! oc))) in - SOME (File.write_list pfile (rev (Unsynchronized.! oc))) handle _ => NONE + try (fn () => File.write_list pfile (rev (Unsynchronized.! oc))) () end fun outStand1 f = outFile1 f (Unsynchronized.! stdout_file) end \ subsection\Interface with Types\ datatype ml_int = ML_int code_printing type_constructor ml_int \ (Haskell) "CodeType.MlInt" \ \syntax!\ | type_constructor ml_int \ (OCaml) "CodeType.mlInt" | type_constructor ml_int \ (Scala) "CodeType.mlInt" | type_constructor ml_int \ (SML) "CodeType.mlInt" datatype 'a ml_monad = ML_monad 'a code_printing type_constructor ml_monad \ (Haskell) "CodeType.MlMonad _" \ \syntax!\ | type_constructor ml_monad \ (OCaml) "_ CodeType.mlMonad" | type_constructor ml_monad \ (Scala) "CodeType.mlMonad [_]" | type_constructor ml_monad \ (SML) "_ CodeType.mlMonad" type_synonym ml_string = String.literal subsection\Interface with Constants\ text\module CodeConst\ consts out_file1 :: "((ml_string \ '\1 \ unit ml_monad) \ \fprintf\ \ unit ml_monad) \ ml_string \ unit ml_monad" code_printing constant out_file1 \ (Haskell) "CodeConst.outFile1" | constant out_file1 \ (OCaml) "CodeConst.outFile1" | constant out_file1 \ (Scala) "CodeConst.outFile1" | constant out_file1 \ (SML) "CodeConst.outFile1" consts out_stand1 :: "((ml_string \ '\1 \ unit ml_monad) \ \fprintf\ \ unit ml_monad) \ unit ml_monad" code_printing constant out_stand1 \ (Haskell) "CodeConst.outStand1" | constant out_stand1 \ (OCaml) "CodeConst.outStand1" | constant out_stand1 \ (Scala) "CodeConst.outStand1" | constant out_stand1 \ (SML) "CodeConst.outStand1" text\module Monad\ consts bind :: "'a ml_monad \ ('a \ 'b ml_monad) \ 'b ml_monad" code_printing constant bind \ (Haskell) "CodeConst.Monad.bind" | constant bind \ (OCaml) "CodeConst.Monad.bind" | constant bind \ (Scala) "CodeConst.Monad.bind" | constant bind \ (SML) "CodeConst.Monad.bind" consts return :: "'a \ 'a ml_monad" code_printing constant return \ (Haskell) "CodeConst.Monad.return" | constant return \ (OCaml) "CodeConst.Monad.return" | constant return \ (Scala) "CodeConst.Monad.Return" \ \syntax!\ | constant return \ (SML) "CodeConst.Monad.return" text\module Printf\ consts sprintf0 :: "ml_string \ ml_string" code_printing constant sprintf0 \ (Haskell) "CodeConst.Printf.sprintf0" | constant sprintf0 \ (OCaml) "CodeConst.Printf.sprintf0" | constant sprintf0 \ (Scala) "CodeConst.Printf.sprintf0" | constant sprintf0 \ (SML) "CodeConst.Printf.sprintf0" consts sprintf1 :: "ml_string \ '\1 \ ml_string" code_printing constant sprintf1 \ (Haskell) "CodeConst.Printf.sprintf1" | constant sprintf1 \ (OCaml) "CodeConst.Printf.sprintf1" | constant sprintf1 \ (Scala) "CodeConst.Printf.sprintf1" | constant sprintf1 \ (SML) "CodeConst.Printf.sprintf1" consts sprintf2 :: "ml_string \ '\1 \ '\2 \ ml_string" code_printing constant sprintf2 \ (Haskell) "CodeConst.Printf.sprintf2" | constant sprintf2 \ (OCaml) "CodeConst.Printf.sprintf2" | constant sprintf2 \ (Scala) "CodeConst.Printf.sprintf2" | constant sprintf2 \ (SML) "CodeConst.Printf.sprintf2" consts sprintf3 :: "ml_string \ '\1 \ '\2 \ '\3 \ ml_string" code_printing constant sprintf3 \ (Haskell) "CodeConst.Printf.sprintf3" | constant sprintf3 \ (OCaml) "CodeConst.Printf.sprintf3" | constant sprintf3 \ (Scala) "CodeConst.Printf.sprintf3" | constant sprintf3 \ (SML) "CodeConst.Printf.sprintf3" consts sprintf4 :: "ml_string \ '\1 \ '\2 \ '\3 \ '\4 \ ml_string" code_printing constant sprintf4 \ (Haskell) "CodeConst.Printf.sprintf4" | constant sprintf4 \ (OCaml) "CodeConst.Printf.sprintf4" | constant sprintf4 \ (Scala) "CodeConst.Printf.sprintf4" | constant sprintf4 \ (SML) "CodeConst.Printf.sprintf4" consts sprintf5 :: "ml_string \ '\1 \ '\2 \ '\3 \ '\4 \ '\5 \ ml_string" code_printing constant sprintf5 \ (Haskell) "CodeConst.Printf.sprintf5" | constant sprintf5 \ (OCaml) "CodeConst.Printf.sprintf5" | constant sprintf5 \ (Scala) "CodeConst.Printf.sprintf5" | constant sprintf5 \ (SML) "CodeConst.Printf.sprintf5" text\module String\ consts String_concat :: "ml_string \ ml_string list \ ml_string" code_printing constant String_concat \ (Haskell) "CodeConst.String.concat" | constant String_concat \ (OCaml) "CodeConst.String.concat" | constant String_concat \ (Scala) "CodeConst.String.concat" | constant String_concat \ (SML) "CodeConst.String.concat" text\module Sys\ consts Sys_is_directory2 :: "ml_string \ bool ml_monad" code_printing constant Sys_is_directory2 \ (Haskell) "CodeConst.Sys.isDirectory2" | constant Sys_is_directory2 \ (OCaml) "CodeConst.Sys.isDirectory2" | constant Sys_is_directory2 \ (Scala) "CodeConst.Sys.isDirectory2" | constant Sys_is_directory2 \ (SML) "CodeConst.Sys.isDirectory2" text\module To\ consts ToNat :: "(nat \ integer) \ nat \ ml_int" code_printing constant ToNat \ (Haskell) "CodeConst.To.nat" | constant ToNat \ (OCaml) "CodeConst.To.nat" | constant ToNat \ (Scala) "CodeConst.To.nat" | constant ToNat \ (SML) "CodeConst.To.nat" subsection\Some Notations (I): Raw Translations\ syntax "_sprint0" :: "_ \ ml_string" ("sprint0 (_)\") translations "sprint0 x\" \ "CONST sprintf0 x" syntax "_sprint1" :: "_ \ _ \ ml_string" ("sprint1 (_)\") translations "sprint1 x\" \ "CONST sprintf1 x" syntax "_sprint2" :: "_ \ _ \ ml_string" ("sprint2 (_)\") translations "sprint2 x\" \ "CONST sprintf2 x" syntax "_sprint3" :: "_ \ _ \ ml_string" ("sprint3 (_)\") translations "sprint3 x\" \ "CONST sprintf3 x" syntax "_sprint4" :: "_ \ _ \ ml_string" ("sprint4 (_)\") translations "sprint4 x\" \ "CONST sprintf4 x" syntax "_sprint5" :: "_ \ _ \ ml_string" ("sprint5 (_)\") translations "sprint5 x\" \ "CONST sprintf5 x" subsection\Some Notations (II): Polymorphic Cartouches\ syntax "_cartouche_string'" :: String.literal translations "_cartouche_string" \ "_cartouche_string'" parse_translation \ [( @{syntax_const "_cartouche_string'"} , parse_translation_cartouche @{binding cartouche_type'} (( "fun\<^sub>p\<^sub>r\<^sub>i\<^sub>n\<^sub>t\<^sub>f" , ( Cartouche_Grammar.nil1 , Cartouche_Grammar.cons1 , let fun f c x = Syntax.const c $ x in fn (0, x) => x | (1, x) => f @{const_syntax sprintf1} x | (2, x) => f @{const_syntax sprintf2} x | (3, x) => f @{const_syntax sprintf3} x | (4, x) => f @{const_syntax sprintf4} x | (5, x) => f @{const_syntax sprintf5} x end)) :: Cartouche_Grammar.default) (fn 37 \ \\<^verbatim>\#"%"\\ => (fn x => x + 1) | _ => I) 0)] \ subsection\Generic Locale for Printing\ locale Print = fixes To_string :: "string \ ml_string" fixes To_nat :: "nat \ ml_int" begin declare[[cartouche_type' = "fun\<^sub>p\<^sub>r\<^sub>i\<^sub>n\<^sub>t\<^sub>f"]] end text\As remark, printing functions (like @{term sprintf5}...) are currently weakly typed in Isabelle, we will continue the typing using the type system of target languages.\ end diff --git a/thys/Native_Word/Uint64.thy b/thys/Native_Word/Uint64.thy --- a/thys/Native_Word/Uint64.thy +++ b/thys/Native_Word/Uint64.thy @@ -1,889 +1,889 @@ (* Title: Uint64.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Unsigned words of 64 bits\ theory Uint64 imports Word_Type_Copies Code_Target_Integer_Bit begin text \ PolyML (in version 5.7) provides a Word64 structure only when run in 64-bit mode. Therefore, we by default provide an implementation of 64-bit words using \verb$IntInf.int$ and masking. The code target \texttt{SML\_word} replaces this implementation and maps the operations directly to the \verb$Word64$ structure provided by the Standard ML implementations. The \verb$Eval$ target used by @{command value} and @{method eval} dynamically tests at runtime for the version of PolyML and uses PolyML's Word64 structure if it detects a 64-bit version which does not suffer from a division bug found in PolyML 5.6. \ section \Type definition and primitive operations\ typedef uint64 = \UNIV :: 64 word set\ .. global_interpretation uint64: word_type_copy Abs_uint64 Rep_uint64 using type_definition_uint64 by (rule word_type_copy.intro) setup_lifting type_definition_uint64 declare uint64.of_word_of [code abstype] declare Quotient_uint64 [transfer_rule] instantiation uint64 :: \{comm_ring_1, semiring_modulo, equal, linorder}\ begin lift_definition zero_uint64 :: uint64 is 0 . lift_definition one_uint64 :: uint64 is 1 . lift_definition plus_uint64 :: \uint64 \ uint64 \ uint64\ is \(+)\ . lift_definition uminus_uint64 :: \uint64 \ uint64\ is uminus . lift_definition minus_uint64 :: \uint64 \ uint64 \ uint64\ is \(-)\ . lift_definition times_uint64 :: \uint64 \ uint64 \ uint64\ is \(*)\ . lift_definition divide_uint64 :: \uint64 \ uint64 \ uint64\ is \(div)\ . lift_definition modulo_uint64 :: \uint64 \ uint64 \ uint64\ is \(mod)\ . lift_definition equal_uint64 :: \uint64 \ uint64 \ bool\ is \HOL.equal\ . lift_definition less_eq_uint64 :: \uint64 \ uint64 \ bool\ is \(\)\ . lift_definition less_uint64 :: \uint64 \ uint64 \ bool\ is \(<)\ . global_interpretation uint64: word_type_copy_ring Abs_uint64 Rep_uint64 by standard (fact zero_uint64.rep_eq one_uint64.rep_eq plus_uint64.rep_eq uminus_uint64.rep_eq minus_uint64.rep_eq times_uint64.rep_eq divide_uint64.rep_eq modulo_uint64.rep_eq equal_uint64.rep_eq less_eq_uint64.rep_eq less_uint64.rep_eq)+ instance proof - show \OFCLASS(uint64, comm_ring_1_class)\ by (rule uint64.of_class_comm_ring_1) show \OFCLASS(uint64, semiring_modulo_class)\ by (fact uint64.of_class_semiring_modulo) show \OFCLASS(uint64, equal_class)\ by (fact uint64.of_class_equal) show \OFCLASS(uint64, linorder_class)\ by (fact uint64.of_class_linorder) qed end instantiation uint64 :: ring_bit_operations begin lift_definition bit_uint64 :: \uint64 \ nat \ bool\ is bit . lift_definition not_uint64 :: \uint64 \ uint64\ is \Bit_Operations.not\ . lift_definition and_uint64 :: \uint64 \ uint64 \ uint64\ is \Bit_Operations.and\ . lift_definition or_uint64 :: \uint64 \ uint64 \ uint64\ is \Bit_Operations.or\ . lift_definition xor_uint64 :: \uint64 \ uint64 \ uint64\ is \Bit_Operations.xor\ . lift_definition mask_uint64 :: \nat \ uint64\ is mask . lift_definition push_bit_uint64 :: \nat \ uint64 \ uint64\ is push_bit . lift_definition drop_bit_uint64 :: \nat \ uint64 \ uint64\ is drop_bit . lift_definition signed_drop_bit_uint64 :: \nat \ uint64 \ uint64\ is signed_drop_bit . lift_definition take_bit_uint64 :: \nat \ uint64 \ uint64\ is take_bit . lift_definition set_bit_uint64 :: \nat \ uint64 \ uint64\ is Bit_Operations.set_bit . lift_definition unset_bit_uint64 :: \nat \ uint64 \ uint64\ is unset_bit . lift_definition flip_bit_uint64 :: \nat \ uint64 \ uint64\ is flip_bit . global_interpretation uint64: word_type_copy_bits Abs_uint64 Rep_uint64 signed_drop_bit_uint64 by standard (fact bit_uint64.rep_eq not_uint64.rep_eq and_uint64.rep_eq or_uint64.rep_eq xor_uint64.rep_eq mask_uint64.rep_eq push_bit_uint64.rep_eq drop_bit_uint64.rep_eq signed_drop_bit_uint64.rep_eq take_bit_uint64.rep_eq set_bit_uint64.rep_eq unset_bit_uint64.rep_eq flip_bit_uint64.rep_eq)+ instance by (fact uint64.of_class_ring_bit_operations) end lift_definition uint64_of_nat :: \nat \ uint64\ is word_of_nat . lift_definition nat_of_uint64 :: \uint64 \ nat\ is unat . lift_definition uint64_of_int :: \int \ uint64\ is word_of_int . lift_definition int_of_uint64 :: \uint64 \ int\ is uint . context includes integer.lifting begin lift_definition Uint64 :: \integer \ uint64\ is word_of_int . lift_definition integer_of_uint64 :: \uint64 \ integer\ is uint . end global_interpretation uint64: word_type_copy_more Abs_uint64 Rep_uint64 signed_drop_bit_uint64 uint64_of_nat nat_of_uint64 uint64_of_int int_of_uint64 Uint64 integer_of_uint64 apply standard apply (simp_all add: uint64_of_nat.rep_eq nat_of_uint64.rep_eq uint64_of_int.rep_eq int_of_uint64.rep_eq Uint64.rep_eq integer_of_uint64.rep_eq integer_eq_iff) done instantiation uint64 :: "{size, msb, lsb, set_bit, bit_comprehension}" begin lift_definition size_uint64 :: \uint64 \ nat\ is size . lift_definition msb_uint64 :: \uint64 \ bool\ is msb . lift_definition lsb_uint64 :: \uint64 \ bool\ is lsb . text \Workaround: avoid name space clash by spelling out \<^text>\lift_definition\ explicitly.\ definition set_bit_uint64 :: \uint64 \ nat \ bool \ uint64\ where set_bit_uint64_eq: \set_bit_uint64 a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\ context includes lifting_syntax begin lemma set_bit_uint64_transfer [transfer_rule]: \(cr_uint64 ===> (=) ===> (\) ===> cr_uint64) Generic_set_bit.set_bit Generic_set_bit.set_bit\ by (simp only: set_bit_eq [abs_def] set_bit_uint64_eq [abs_def]) transfer_prover end lift_definition set_bits_uint64 :: \(nat \ bool) \ uint64\ is set_bits . lift_definition set_bits_aux_uint64 :: \(nat \ bool) \ nat \ uint64 \ uint64\ is set_bits_aux . global_interpretation uint64: word_type_copy_misc Abs_uint64 Rep_uint64 signed_drop_bit_uint64 uint64_of_nat nat_of_uint64 uint64_of_int int_of_uint64 Uint64 integer_of_uint64 64 set_bits_aux_uint64 by (standard; transfer) simp_all instance using uint64.of_class_bit_comprehension uint64.of_class_set_bit uint64.of_class_lsb by simp_all standard end section \Code setup\ text \ For SML, we generate an implementation of unsigned 64-bit words using \verb$IntInf.int$. If @{ML "LargeWord.wordSize > 63"} of the Isabelle/ML runtime environment holds, then we assume that there is also a \Word64\ structure available and accordingly replace the implementation for the target \verb$Eval$. \ code_printing code_module "Uint64" \ (SML) \(* Test that words can handle numbers between 0 and 63 *) val _ = if 6 <= Word.wordSize then () else raise (Fail ("wordSize less than 6")); structure Uint64 : sig eqtype uint64; val zero : uint64; val one : uint64; val fromInt : IntInf.int -> uint64; val toInt : uint64 -> IntInf.int; val toLarge : uint64 -> LargeWord.word; val fromLarge : LargeWord.word -> uint64 val plus : uint64 -> uint64 -> uint64; val minus : uint64 -> uint64 -> uint64; val times : uint64 -> uint64 -> uint64; val divide : uint64 -> uint64 -> uint64; val modulus : uint64 -> uint64 -> uint64; val negate : uint64 -> uint64; val less_eq : uint64 -> uint64 -> bool; val less : uint64 -> uint64 -> bool; val notb : uint64 -> uint64; val andb : uint64 -> uint64 -> uint64; val orb : uint64 -> uint64 -> uint64; val xorb : uint64 -> uint64 -> uint64; val shiftl : uint64 -> IntInf.int -> uint64; val shiftr : uint64 -> IntInf.int -> uint64; val shiftr_signed : uint64 -> IntInf.int -> uint64; val set_bit : uint64 -> IntInf.int -> bool -> uint64; val test_bit : uint64 -> IntInf.int -> bool; end = struct type uint64 = IntInf.int; val mask = 0xFFFFFFFFFFFFFFFF : IntInf.int; val zero = 0 : IntInf.int; val one = 1 : IntInf.int; fun fromInt x = IntInf.andb(x, mask); fun toInt x = x fun toLarge x = LargeWord.fromLargeInt (IntInf.toLarge x); fun fromLarge x = IntInf.fromLarge (LargeWord.toLargeInt x); fun plus x y = IntInf.andb(IntInf.+(x, y), mask); fun minus x y = IntInf.andb(IntInf.-(x, y), mask); fun negate x = IntInf.andb(IntInf.~(x), mask); fun times x y = IntInf.andb(IntInf.*(x, y), mask); fun divide x y = IntInf.div(x, y); fun modulus x y = IntInf.mod(x, y); fun less_eq x y = IntInf.<=(x, y); fun less x y = IntInf.<(x, y); fun notb x = IntInf.andb(IntInf.notb(x), mask); fun orb x y = IntInf.orb(x, y); fun andb x y = IntInf.andb(x, y); fun xorb x y = IntInf.xorb(x, y); val maxWord = IntInf.pow (2, Word.wordSize); fun shiftl x n = if n < maxWord then IntInf.andb(IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n)), mask) else 0; fun shiftr x n = if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n)) else 0; val msb_mask = 0x8000000000000000 : IntInf.int; fun shiftr_signed x i = if IntInf.andb(x, msb_mask) = 0 then shiftr x i else if i >= 64 then 0xFFFFFFFFFFFFFFFF else let val x' = shiftr x i val m' = IntInf.andb(IntInf.<<(mask, Word.max(0w64 - Word.fromLargeInt (IntInf.toLarge i), 0w0)), mask) in IntInf.orb(x', m') end; fun test_bit x n = if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0 else false; fun set_bit x n b = if n < 64 then if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))) else x; end \ code_reserved SML Uint64 setup \ let val polyml64 = LargeWord.wordSize > 63; (* PolyML 5.6 has bugs in its Word64 implementation. We test for one such bug and refrain from using Word64 in that case. Testing is done with dynamic code evaluation such that the compiler does not choke on the Word64 structure, which need not be present in a 32bit environment. *) val error_msg = "Buggy Word64 structure"; val test_code = "val _ = if Word64.div (0w18446744073709551611 : Word64.word, 0w3) = 0w6148914691236517203 then ()\n" ^ "else raise (Fail \"" ^ error_msg ^ "\");"; - val f = Exn.interruptible_capture (fn () => ML_Compiler.eval ML_Compiler.flags Position.none (ML_Lex.tokenize test_code)) + val f = Exn.result (fn () => ML_Compiler.eval ML_Compiler.flags Position.none (ML_Lex.tokenize test_code)) val use_Word64 = polyml64 andalso (case f () of Exn.Res _ => true | Exn.Exn (e as ERROR m) => if String.isSuffix error_msg m then false else Exn.reraise e | Exn.Exn e => Exn.reraise e) ; val newline = "\n"; val content = "structure Uint64 : sig" ^ newline ^ " eqtype uint64;" ^ newline ^ " val zero : uint64;" ^ newline ^ " val one : uint64;" ^ newline ^ " val fromInt : IntInf.int -> uint64;" ^ newline ^ " val toInt : uint64 -> IntInf.int;" ^ newline ^ " val toLarge : uint64 -> LargeWord.word;" ^ newline ^ " val fromLarge : LargeWord.word -> uint64" ^ newline ^ " val plus : uint64 -> uint64 -> uint64;" ^ newline ^ " val minus : uint64 -> uint64 -> uint64;" ^ newline ^ " val times : uint64 -> uint64 -> uint64;" ^ newline ^ " val divide : uint64 -> uint64 -> uint64;" ^ newline ^ " val modulus : uint64 -> uint64 -> uint64;" ^ newline ^ " val negate : uint64 -> uint64;" ^ newline ^ " val less_eq : uint64 -> uint64 -> bool;" ^ newline ^ " val less : uint64 -> uint64 -> bool;" ^ newline ^ " val notb : uint64 -> uint64;" ^ newline ^ " val andb : uint64 -> uint64 -> uint64;" ^ newline ^ " val orb : uint64 -> uint64 -> uint64;" ^ newline ^ " val xorb : uint64 -> uint64 -> uint64;" ^ newline ^ " val shiftl : uint64 -> IntInf.int -> uint64;" ^ newline ^ " val shiftr : uint64 -> IntInf.int -> uint64;" ^ newline ^ " val shiftr_signed : uint64 -> IntInf.int -> uint64;" ^ newline ^ " val set_bit : uint64 -> IntInf.int -> bool -> uint64;" ^ newline ^ " val test_bit : uint64 -> IntInf.int -> bool;" ^ newline ^ "end = struct" ^ newline ^ "" ^ newline ^ "type uint64 = Word64.word;" ^ newline ^ "" ^ newline ^ "val zero = (0wx0 : uint64);" ^ newline ^ "" ^ newline ^ "val one = (0wx1 : uint64);" ^ newline ^ "" ^ newline ^ "fun fromInt x = Word64.fromLargeInt (IntInf.toLarge x);" ^ newline ^ "" ^ newline ^ "fun toInt x = IntInf.fromLarge (Word64.toLargeInt x);" ^ newline ^ "" ^ newline ^ "fun fromLarge x = Word64.fromLarge x;" ^ newline ^ "" ^ newline ^ "fun toLarge x = Word64.toLarge x;" ^ newline ^ "" ^ newline ^ "fun plus x y = Word64.+(x, y);" ^ newline ^ "" ^ newline ^ "fun minus x y = Word64.-(x, y);" ^ newline ^ "" ^ newline ^ "fun negate x = Word64.~(x);" ^ newline ^ "" ^ newline ^ "fun times x y = Word64.*(x, y);" ^ newline ^ "" ^ newline ^ "fun divide x y = Word64.div(x, y);" ^ newline ^ "" ^ newline ^ "fun modulus x y = Word64.mod(x, y);" ^ newline ^ "" ^ newline ^ "fun less_eq x y = Word64.<=(x, y);" ^ newline ^ "" ^ newline ^ "fun less x y = Word64.<(x, y);" ^ newline ^ "" ^ newline ^ "fun set_bit x n b =" ^ newline ^ " let val mask = Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ " in if b then Word64.orb (x, mask)" ^ newline ^ " else Word64.andb (x, Word64.notb mask)" ^ newline ^ " end" ^ newline ^ "" ^ newline ^ "fun shiftl x n =" ^ newline ^ " Word64.<< (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ "" ^ newline ^ "fun shiftr x n =" ^ newline ^ " Word64.>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ "" ^ newline ^ "fun shiftr_signed x n =" ^ newline ^ " Word64.~>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ "" ^ newline ^ "fun test_bit x n =" ^ newline ^ " Word64.andb (x, Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word64.fromInt 0" ^ newline ^ "" ^ newline ^ "val notb = Word64.notb" ^ newline ^ "" ^ newline ^ "fun andb x y = Word64.andb(x, y);" ^ newline ^ "" ^ newline ^ "fun orb x y = Word64.orb(x, y);" ^ newline ^ "" ^ newline ^ "fun xorb x y = Word64.xorb(x, y);" ^ newline ^ "" ^ newline ^ "end (*struct Uint64*)" val target_SML64 = "SML_word"; in (if use_Word64 then Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(Code_Runtime.target, SOME (content, []))])) else I) #> Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(target_SML64, SOME (content, []))])) end \ code_printing code_module Uint64 \ (Haskell) \module Uint64(Int64, Word64) where import Data.Int(Int64) import Data.Word(Word64)\ code_reserved Haskell Uint64 text \ OCaml and Scala provide only signed 64bit numbers, so we use these and implement sign-sensitive operations like comparisons manually. \ code_printing code_module "Uint64" \ (OCaml) \module Uint64 : sig val less : int64 -> int64 -> bool val less_eq : int64 -> int64 -> bool val set_bit : int64 -> Z.t -> bool -> int64 val shiftl : int64 -> Z.t -> int64 val shiftr : int64 -> Z.t -> int64 val shiftr_signed : int64 -> Z.t -> int64 val test_bit : int64 -> Z.t -> bool end = struct (* negative numbers have their highest bit set, so they are greater than positive ones *) let less x y = if Int64.compare x Int64.zero < 0 then Int64.compare y Int64.zero < 0 && Int64.compare x y < 0 else Int64.compare y Int64.zero < 0 || Int64.compare x y < 0;; let less_eq x y = if Int64.compare x Int64.zero < 0 then Int64.compare y Int64.zero < 0 && Int64.compare x y <= 0 else Int64.compare y Int64.zero < 0 || Int64.compare x y <= 0;; let set_bit x n b = let mask = Int64.shift_left Int64.one (Z.to_int n) in if b then Int64.logor x mask else Int64.logand x (Int64.lognot mask);; let shiftl x n = Int64.shift_left x (Z.to_int n);; let shiftr x n = Int64.shift_right_logical x (Z.to_int n);; let shiftr_signed x n = Int64.shift_right x (Z.to_int n);; let test_bit x n = Int64.compare (Int64.logand x (Int64.shift_left Int64.one (Z.to_int n))) Int64.zero <> 0;; end;; (*struct Uint64*)\ code_reserved OCaml Uint64 code_printing code_module Uint64 \ (Scala) \object Uint64 { def less(x: Long, y: Long) : Boolean = if (x < 0) y < 0 && x < y else y < 0 || x < y def less_eq(x: Long, y: Long) : Boolean = if (x < 0) y < 0 && x <= y else y < 0 || x <= y def set_bit(x: Long, n: BigInt, b: Boolean) : Long = if (b) x | (1L << n.intValue) else x & (1L << n.intValue).unary_~ def shiftl(x: Long, n: BigInt) : Long = x << n.intValue def shiftr(x: Long, n: BigInt) : Long = x >>> n.intValue def shiftr_signed(x: Long, n: BigInt) : Long = x >> n.intValue def test_bit(x: Long, n: BigInt) : Boolean = (x & (1L << n.intValue)) != 0 } /* object Uint64 */\ code_reserved Scala Uint64 text \ OCaml's conversion from Big\_int to int64 demands that the value fits int a signed 64-bit integer. The following justifies the implementation. \ context includes bit_operations_syntax begin definition Uint64_signed :: "integer \ uint64" where "Uint64_signed i = (if i < -(0x8000000000000000) \ i \ 0x8000000000000000 then undefined Uint64 i else Uint64 i)" lemma Uint64_code [code]: "Uint64 i = (let i' = i AND 0xFFFFFFFFFFFFFFFF in if bit i' 63 then Uint64_signed (i' - 0x10000000000000000) else Uint64_signed i')" including undefined_transfer integer.lifting unfolding Uint64_signed_def apply transfer apply (subst word_of_int_via_signed) apply (auto simp add: push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed cong del: if_cong) done lemma Uint64_signed_code [code]: "Rep_uint64 (Uint64_signed i) = (if i < -(0x8000000000000000) \ i \ 0x8000000000000000 then Rep_uint64 (undefined Uint64 i) else word_of_int (int_of_integer_symbolic i))" unfolding Uint64_signed_def Uint64_def int_of_integer_symbolic_def by(simp add: Abs_uint64_inverse) end text \ Avoid @{term Abs_uint64} in generated code, use @{term Rep_uint64'} instead. The symbolic implementations for code\_simp use @{term Rep_uint64}. The new destructor @{term Rep_uint64'} is executable. As the simplifier is given the [code abstract] equations literally, we cannot implement @{term Rep_uint64} directly, because that makes code\_simp loop. If code generation raises Match, some equation probably contains @{term Rep_uint64} ([code abstract] equations for @{typ uint64} may use @{term Rep_uint64} because these instances will be folded away.) To convert @{typ "64 word"} values into @{typ uint64}, use @{term "Abs_uint64'"}. \ definition Rep_uint64' where [simp]: "Rep_uint64' = Rep_uint64" lemma Rep_uint64'_transfer [transfer_rule]: "rel_fun cr_uint64 (=) (\x. x) Rep_uint64'" unfolding Rep_uint64'_def by(rule uint64.rep_transfer) lemma Rep_uint64'_code [code]: "Rep_uint64' x = (BITS n. bit x n)" by transfer (simp add: set_bits_bit_eq) lift_definition Abs_uint64' :: "64 word \ uint64" is "\x :: 64 word. x" . lemma Abs_uint64'_code [code]: "Abs_uint64' x = Uint64 (integer_of_int (uint x))" including integer.lifting by transfer simp declare [[code drop: "term_of_class.term_of :: uint64 \ _"]] lemma term_of_uint64_code [code]: defines "TR \ typerep.Typerep" and "bit0 \ STR ''Numeral_Type.bit0''" shows "term_of_class.term_of x = Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint64.uint64.Abs_uint64'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]]], TR (STR ''Uint64.uint64'') []])) (term_of_class.term_of (Rep_uint64' x))" by(simp add: term_of_anything) code_printing type_constructor uint64 \ (SML) "Uint64.uint64" and (Haskell) "Uint64.Word64" and (OCaml) "int64" and (Scala) "Long" | constant Uint64 \ (SML) "Uint64.fromInt" and (Haskell) "(Prelude.fromInteger _ :: Uint64.Word64)" and (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Word64)" and (Scala) "_.longValue" | constant Uint64_signed \ (OCaml) "Z.to'_int64" | constant "0 :: uint64" \ (SML) "Uint64.zero" and (Haskell) "(0 :: Uint64.Word64)" and (OCaml) "Int64.zero" and (Scala) "0" | constant "1 :: uint64" \ (SML) "Uint64.one" and (Haskell) "(1 :: Uint64.Word64)" and (OCaml) "Int64.one" and (Scala) "1" | constant "plus :: uint64 \ _ " \ (SML) "Uint64.plus" and (Haskell) infixl 6 "+" and (OCaml) "Int64.add" and (Scala) infixl 7 "+" | constant "uminus :: uint64 \ _" \ (SML) "Uint64.negate" and (Haskell) "negate" and (OCaml) "Int64.neg" and (Scala) "!(- _)" | constant "minus :: uint64 \ _" \ (SML) "Uint64.minus" and (Haskell) infixl 6 "-" and (OCaml) "Int64.sub" and (Scala) infixl 7 "-" | constant "times :: uint64 \ _ \ _" \ (SML) "Uint64.times" and (Haskell) infixl 7 "*" and (OCaml) "Int64.mul" and (Scala) infixl 8 "*" | constant "HOL.equal :: uint64 \ _ \ bool" \ (SML) "!((_ : Uint64.uint64) = _)" and (Haskell) infix 4 "==" and (OCaml) "(Int64.compare _ _ = 0)" and (Scala) infixl 5 "==" | class_instance uint64 :: equal \ (Haskell) - | constant "less_eq :: uint64 \ _ \ bool" \ (SML) "Uint64.less'_eq" and (Haskell) infix 4 "<=" and (OCaml) "Uint64.less'_eq" and (Scala) "Uint64.less'_eq" | constant "less :: uint64 \ _ \ bool" \ (SML) "Uint64.less" and (Haskell) infix 4 "<" and (OCaml) "Uint64.less" and (Scala) "Uint64.less" | constant "Bit_Operations.not :: uint64 \ _" \ (SML) "Uint64.notb" and (Haskell) "Data'_Bits.complement" and (OCaml) "Int64.lognot" and (Scala) "_.unary'_~" | constant "Bit_Operations.and :: uint64 \ _" \ (SML) "Uint64.andb" and (Haskell) infixl 7 "Data_Bits..&." and (OCaml) "Int64.logand" and (Scala) infixl 3 "&" | constant "Bit_Operations.or :: uint64 \ _" \ (SML) "Uint64.orb" and (Haskell) infixl 5 "Data_Bits..|." and (OCaml) "Int64.logor" and (Scala) infixl 1 "|" | constant "Bit_Operations.xor :: uint64 \ _" \ (SML) "Uint64.xorb" and (Haskell) "Data'_Bits.xor" and (OCaml) "Int64.logxor" and (Scala) infixl 2 "^" definition uint64_divmod :: "uint64 \ uint64 \ uint64 \ uint64" where "uint64_divmod x y = (if y = 0 then (undefined ((div) :: uint64 \ _) x (0 :: uint64), undefined ((mod) :: uint64 \ _) x (0 :: uint64)) else (x div y, x mod y))" definition uint64_div :: "uint64 \ uint64 \ uint64" where "uint64_div x y = fst (uint64_divmod x y)" definition uint64_mod :: "uint64 \ uint64 \ uint64" where "uint64_mod x y = snd (uint64_divmod x y)" lemma div_uint64_code [code]: "x div y = (if y = 0 then 0 else uint64_div x y)" including undefined_transfer unfolding uint64_divmod_def uint64_div_def by transfer (simp add: word_div_def) lemma mod_uint64_code [code]: "x mod y = (if y = 0 then x else uint64_mod x y)" including undefined_transfer unfolding uint64_mod_def uint64_divmod_def by transfer (simp add: word_mod_def) definition uint64_sdiv :: "uint64 \ uint64 \ uint64" where [code del]: "uint64_sdiv x y = (if y = 0 then undefined ((div) :: uint64 \ _) x (0 :: uint64) else Abs_uint64 (Rep_uint64 x sdiv Rep_uint64 y))" definition div0_uint64 :: "uint64 \ uint64" where [code del]: "div0_uint64 x = undefined ((div) :: uint64 \ _) x (0 :: uint64)" declare [[code abort: div0_uint64]] definition mod0_uint64 :: "uint64 \ uint64" where [code del]: "mod0_uint64 x = undefined ((mod) :: uint64 \ _) x (0 :: uint64)" declare [[code abort: mod0_uint64]] lemma uint64_divmod_code [code]: "uint64_divmod x y = (if 0x8000000000000000 \ y then if x < y then (0, x) else (1, x - y) else if y = 0 then (div0_uint64 x, mod0_uint64 x) else let q = push_bit 1 (uint64_sdiv (drop_bit 1 x) y); r = x - q * y in if r \ y then (q + 1, r - y) else (q, r))" including undefined_transfer unfolding uint64_divmod_def uint64_sdiv_def div0_uint64_def mod0_uint64_def less_eq_uint64.rep_eq apply transfer apply (simp add: divmod_via_sdivmod push_bit_eq_mult) done lemma uint64_sdiv_code [code]: "Rep_uint64 (uint64_sdiv x y) = (if y = 0 then Rep_uint64 (undefined ((div) :: uint64 \ _) x (0 :: uint64)) else Rep_uint64 x sdiv Rep_uint64 y)" unfolding uint64_sdiv_def by(simp add: Abs_uint64_inverse) text \ Note that we only need a translation for signed division, but not for the remainder because @{thm uint64_divmod_code} computes both with division only. \ code_printing constant uint64_div \ (SML) "Uint64.divide" and (Haskell) "Prelude.div" | constant uint64_mod \ (SML) "Uint64.modulus" and (Haskell) "Prelude.mod" | constant uint64_divmod \ (Haskell) "divmod" | constant uint64_sdiv \ (OCaml) "Int64.div" and (Scala) "_ '/ _" definition uint64_test_bit :: "uint64 \ integer \ bool" where [code del]: "uint64_test_bit x n = (if n < 0 \ 63 < n then undefined (bit :: uint64 \ _) x n else bit x (nat_of_integer n))" lemma bit_uint64_code [code]: "bit x n \ n < 64 \ uint64_test_bit x (integer_of_nat n)" including undefined_transfer integer.lifting unfolding uint64_test_bit_def by transfer (auto dest: bit_imp_le_length) lemma uint64_test_bit_code [code]: "uint64_test_bit w n = (if n < 0 \ 63 < n then undefined (bit :: uint64 \ _) w n else bit (Rep_uint64 w) (nat_of_integer n))" unfolding uint64_test_bit_def by(simp add: bit_uint64.rep_eq) code_printing constant uint64_test_bit \ (SML) "Uint64.test'_bit" and (Haskell) "Data'_Bits.testBitBounded" and (OCaml) "Uint64.test'_bit" and (Scala) "Uint64.test'_bit" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_test'_bit out of bounds\") else Uint64.test'_bit x i)" definition uint64_set_bit :: "uint64 \ integer \ bool \ uint64" where [code del]: "uint64_set_bit x n b = (if n < 0 \ 63 < n then undefined (set_bit :: uint64 \ _) x n b else set_bit x (nat_of_integer n) b)" lemma set_bit_uint64_code [code]: "set_bit x n b = (if n < 64 then uint64_set_bit x (integer_of_nat n) b else x)" including undefined_transfer integer.lifting unfolding uint64_set_bit_def by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size) lemma uint64_set_bit_code [code]: "Rep_uint64 (uint64_set_bit w n b) = (if n < 0 \ 63 < n then Rep_uint64 (undefined (set_bit :: uint64 \ _) w n b) else set_bit (Rep_uint64 w) (nat_of_integer n) b)" including undefined_transfer unfolding uint64_set_bit_def by transfer simp code_printing constant uint64_set_bit \ (SML) "Uint64.set'_bit" and (Haskell) "Data'_Bits.setBitBounded" and (OCaml) "Uint64.set'_bit" and (Scala) "Uint64.set'_bit" and (Eval) "(fn x => fn i => fn b => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_set'_bit out of bounds\") else Uint64.set'_bit x i b)" definition uint64_shiftl :: "uint64 \ integer \ uint64" where [code del]: "uint64_shiftl x n = (if n < 0 \ 64 \ n then undefined (push_bit :: nat \ uint64 \ _) x n else push_bit (nat_of_integer n) x)" lemma shiftl_uint64_code [code]: "push_bit n x = (if n < 64 then uint64_shiftl x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint64_shiftl_def by transfer simp lemma uint64_shiftl_code [code]: "Rep_uint64 (uint64_shiftl w n) = (if n < 0 \ 64 \ n then Rep_uint64 (undefined (push_bit :: nat \ uint64 \ _) w n) else push_bit (nat_of_integer n) (Rep_uint64 w))" including undefined_transfer unfolding uint64_shiftl_def by transfer simp code_printing constant uint64_shiftl \ (SML) "Uint64.shiftl" and (Haskell) "Data'_Bits.shiftlBounded" and (OCaml) "Uint64.shiftl" and (Scala) "Uint64.shiftl" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftl out of bounds\") else Uint64.shiftl x i)" definition uint64_shiftr :: "uint64 \ integer \ uint64" where [code del]: "uint64_shiftr x n = (if n < 0 \ 64 \ n then undefined (drop_bit :: nat \ uint64 \ _) x n else drop_bit (nat_of_integer n) x)" lemma shiftr_uint64_code [code]: "drop_bit n x = (if n < 64 then uint64_shiftr x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint64_shiftr_def by transfer simp lemma uint64_shiftr_code [code]: "Rep_uint64 (uint64_shiftr w n) = (if n < 0 \ 64 \ n then Rep_uint64 (undefined (drop_bit :: nat \ uint64 \ _) w n) else drop_bit (nat_of_integer n) (Rep_uint64 w))" including undefined_transfer unfolding uint64_shiftr_def by transfer simp code_printing constant uint64_shiftr \ (SML) "Uint64.shiftr" and (Haskell) "Data'_Bits.shiftrBounded" and (OCaml) "Uint64.shiftr" and (Scala) "Uint64.shiftr" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr out of bounds\") else Uint64.shiftr x i)" definition uint64_sshiftr :: "uint64 \ integer \ uint64" where [code del]: "uint64_sshiftr x n = (if n < 0 \ 64 \ n then undefined signed_drop_bit_uint64 n x else signed_drop_bit_uint64 (nat_of_integer n) x)" lemma sshiftr_uint64_code [code]: "signed_drop_bit_uint64 n x = (if n < 64 then uint64_sshiftr x (integer_of_nat n) else if bit x 63 then - 1 else 0)" including undefined_transfer integer.lifting unfolding uint64_sshiftr_def by transfer (simp add: not_less signed_drop_bit_beyond) lemma uint64_sshiftr_code [code]: "Rep_uint64 (uint64_sshiftr w n) = (if n < 0 \ 64 \ n then Rep_uint64 (undefined signed_drop_bit_uint64 n w) else signed_drop_bit (nat_of_integer n) (Rep_uint64 w))" including undefined_transfer unfolding uint64_sshiftr_def by transfer simp code_printing constant uint64_sshiftr \ (SML) "Uint64.shiftr'_signed" and (Haskell) "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Int64) _)) :: Uint64.Word64)" and (OCaml) "Uint64.shiftr'_signed" and (Scala) "Uint64.shiftr'_signed" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr'_signed out of bounds\") else Uint64.shiftr'_signed x i)" context includes bit_operations_syntax begin lemma uint64_msb_test_bit: "msb x \ bit (x :: uint64) 63" by transfer (simp add: msb_word_iff_bit) lemma msb_uint64_code [code]: "msb x \ uint64_test_bit x 63" by (simp add: uint64_test_bit_def uint64_msb_test_bit) lemma uint64_of_int_code [code]: "uint64_of_int i = Uint64 (integer_of_int i)" including integer.lifting by transfer simp lemma int_of_uint64_code [code]: "int_of_uint64 x = int_of_integer (integer_of_uint64 x)" including integer.lifting by transfer simp lemma uint64_of_nat_code [code]: "uint64_of_nat = uint64_of_int \ int" by transfer (simp add: fun_eq_iff) lemma nat_of_uint64_code [code]: "nat_of_uint64 x = nat_of_integer (integer_of_uint64 x)" unfolding integer_of_uint64_def including integer.lifting by transfer simp definition integer_of_uint64_signed :: "uint64 \ integer" where "integer_of_uint64_signed n = (if bit n 63 then undefined integer_of_uint64 n else integer_of_uint64 n)" lemma integer_of_uint64_signed_code [code]: "integer_of_uint64_signed n = (if bit n 63 then undefined integer_of_uint64 n else integer_of_int (uint (Rep_uint64' n)))" by (simp add: integer_of_uint64_signed_def integer_of_uint64_def) lemma integer_of_uint64_code [code]: "integer_of_uint64 n = (if bit n 63 then integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 else integer_of_uint64_signed n)" proof - have \integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 = Bit_Operations.set_bit 63 (integer_of_uint64_signed (take_bit 63 n))\ by (simp add: take_bit_eq_mask set_bit_eq_or push_bit_eq_mult mask_eq_exp_minus_1) moreover have \integer_of_uint64 n = Bit_Operations.set_bit 63 (integer_of_uint64 (take_bit 63 n))\ if \bit n 63\ proof (rule bit_eqI) fix m from that show \bit (integer_of_uint64 n) m = bit (Bit_Operations.set_bit 63 (integer_of_uint64 (take_bit 63 n))) m\ for m including integer.lifting by transfer (auto simp add: bit_simps dest: bit_imp_le_length) qed ultimately show ?thesis by simp (simp add: integer_of_uint64_signed_def bit_simps) qed end code_printing constant "integer_of_uint64" \ (SML) "Uint64.toInt" and (Haskell) "Prelude.toInteger" | constant "integer_of_uint64_signed" \ (OCaml) "Z.of'_int64" and (Scala) "BigInt" section \Quickcheck setup\ definition uint64_of_natural :: "natural \ uint64" where "uint64_of_natural x \ Uint64 (integer_of_natural x)" instantiation uint64 :: "{random, exhaustive, full_exhaustive}" begin definition "random_uint64 \ qc_random_cnv uint64_of_natural" definition "exhaustive_uint64 \ qc_exhaustive_cnv uint64_of_natural" definition "full_exhaustive_uint64 \ qc_full_exhaustive_cnv uint64_of_natural" instance .. end instantiation uint64 :: narrowing begin interpretation quickcheck_narrowing_samples "\i. let x = Uint64 i in (x, 0xFFFFFFFFFFFFFFFF - x)" "0" "Typerep.Typerep (STR ''Uint64.uint64'') []" . definition "narrowing_uint64 d = qc_narrowing_drawn_from (narrowing_samples d) d" declare [[code drop: "partial_term_of :: uint64 itself \ _"]] lemmas partial_term_of_uint64 [code] = partial_term_of_code instance .. end end diff --git a/thys/Separation_Logic_Imperative_HOL/Automation.thy b/thys/Separation_Logic_Imperative_HOL/Automation.thy --- a/thys/Separation_Logic_Imperative_HOL/Automation.thy +++ b/thys/Separation_Logic_Imperative_HOL/Automation.thy @@ -1,1066 +1,1065 @@ section \Automation\ theory Automation imports Hoare_Triple (*"../Lib/Refine_Util"*) begin text \ In this theory, we provide a set of tactics and a simplifier setup for easy reasoning with our separation logic. \ subsection \Normalization of Assertions\ text \ In this section, we provide a set of lemmas and a simplifier setup to bring assertions to a normal form. We provide a simproc that detects pure parts of assertions and duplicate pointers. Moreover, we provide ac-rules for assertions. See Section~\ref{sec:auto:overview} for a short overview of the available proof methods. \ lemmas assn_aci = inf_aci[where 'a=assn] sup_aci[where 'a=assn] mult.left_ac[where 'a=assn] lemmas star_assoc = mult.assoc[where 'a=assn] lemmas assn_assoc = mult.left_assoc inf_assoc[where 'a=assn] sup_assoc[where 'a=assn] lemma merge_true_star_ctx: "true * (true * P) = true * P" by (simp add: mult.left_ac) lemmas star_aci = mult.assoc[where 'a=assn] mult.commute[where 'a=assn] mult.left_commute[where 'a=assn] assn_one_left mult_1_right[where 'a=assn] merge_true_star merge_true_star_ctx text \Move existential quantifiers to the front of assertions\ lemma ex_assn_move_out[simp]: "\Q R. (\\<^sub>Ax. Q x) * R = (\\<^sub>Ax. (Q x * R))" "\Q R. R * (\\<^sub>Ax. Q x) = (\\<^sub>Ax. (R * Q x))" "\P Q. (\\<^sub>Ax. Q x) \\<^sub>A P = (\\<^sub>Ax. (Q x \\<^sub>A P)) " "\P Q. Q \\<^sub>A (\\<^sub>Ax. P x) = (\\<^sub>Ax. (Q \\<^sub>A P x))" "\P Q. (\\<^sub>Ax. Q x) \\<^sub>A P = (\\<^sub>Ax. (Q x \\<^sub>A P))" "\P Q. Q \\<^sub>A (\\<^sub>Ax. P x) = (\\<^sub>Ax. (Q \\<^sub>A P x))" apply - apply (simp add: ex_distrib_star) apply (subst mult.commute) apply (subst (2) mult.commute) apply (simp add: ex_distrib_star) apply (simp add: ex_distrib_and) apply (subst inf_commute) apply (subst (2) inf_commute) apply (simp add: ex_distrib_and) apply (simp add: ex_distrib_or) apply (subst sup_commute) apply (subst (2) sup_commute) apply (simp add: ex_distrib_or) done text \Extract pure assertions from and-clauses\ lemma and_extract_pure_left_iff[simp]: "\b \\<^sub>A Q = (emp\\<^sub>AQ)*\b" by (cases b) auto lemma and_extract_pure_left_ctx_iff[simp]: "P*\b \\<^sub>A Q = (P\\<^sub>AQ)*\b" by (cases b) auto lemma and_extract_pure_right_iff[simp]: "P \\<^sub>A \b = (emp\\<^sub>AP)*\b" by (cases b) (auto simp: assn_aci) lemma and_extract_pure_right_ctx_iff[simp]: "P \\<^sub>A Q*\b = (P\\<^sub>AQ)*\b" by (cases b) auto lemmas and_extract_pure_iff = and_extract_pure_left_iff and_extract_pure_left_ctx_iff and_extract_pure_right_iff and_extract_pure_right_ctx_iff lemmas norm_assertion_simps = (* Neutral elements *) mult_1[where 'a=assn] mult_1_right[where 'a=assn] inf_top_left[where 'a=assn] inf_top_right[where 'a=assn] sup_bot_left[where 'a=assn] sup_bot_right[where 'a=assn] (* Zero elements *) star_false_left star_false_right inf_bot_left[where 'a=assn] inf_bot_right[where 'a=assn] sup_top_left[where 'a=assn] sup_top_right[where 'a=assn] (* Associativity *) mult.left_assoc[where 'a=assn] inf_assoc[where 'a=assn] sup_assoc[where 'a=assn] (* Existential Quantifiers *) ex_assn_move_out ex_assn_const (* Extract pure assertions from conjunctions *) and_extract_pure_iff (* Merging *) merge_pure_star merge_pure_and merge_pure_or merge_true_star inf_idem[where 'a=assn] sup_idem[where 'a=assn] (* Duplicated References *) sngr_same_false snga_same_false subsubsection \Simplifier Setup Fine-Tuning\ text \Imperative HOL likes to simplify pointer inequations to this strange operator. We do some additional simplifier setup here\ lemma not_same_noteqr[simp]: "\ a=!=a" by (metis Ref.unequal) declare Ref.noteq_irrefl[dest!] lemma not_same_noteqa[simp]: "\ a=!!=a" by (metis Array.unequal) declare Array.noteq_irrefl[dest!] text \However, it is safest to disable this rewriting, as there is a working standard simplifier setup for \(\)\ \ declare Ref.unequal[simp del] declare Array.unequal[simp del] subsection \Normalization of Entailments\ text \Used by existential quantifier extraction tactic\ lemma enorm_exI': (* Incomplete, as chosen x may depend on heap! *) "(\x. Z x \ (P \\<^sub>A Q x)) \ (\x. Z x) \ (P \\<^sub>A (\\<^sub>Ax. Q x))" by (metis ent_ex_postI) text \Example of how to build an extraction lemma.\ thm enorm_exI'[OF enorm_exI'[OF imp_refl]] lemmas ent_triv = ent_true ent_false text \Dummy rule to detect Hoare triple goal\ lemma is_hoare_triple: "

c \

c " . text \Dummy rule to detect entailment goal\ lemma is_entails: "P\\<^sub>AQ \ P \\<^sub>AQ" . subsection \Frame Matcher\ text \Given star-lists P,Q and a frame F, this method tries to match all elements of Q with corresponding elements of P. The result is a partial match, that contains matching pairs and the unmatched content.\ text \The frame-matcher internally uses syntactic lists separated by star, and delimited by the special symbol \SLN\, which is defined to be \emp\.\ definition [simp]: "SLN \ emp" lemma SLN_left: "SLN * P = P" by simp lemma SLN_right: "P * SLN = P" by simp lemmas SLN_normalize = SLN_right mult.left_assoc[where 'a=assn] lemmas SLN_strip = SLN_right SLN_left mult.left_assoc[where 'a=assn] text \A query to the frame matcher. Contains the assertions P and Q that shall be matched, as well as a frame F, that is not touched.\ definition [simp]: "FI_QUERY P Q F \ P \\<^sub>A Q*F" abbreviation "fi_m_fst M \ foldr (*) (map fst M) emp" abbreviation "fi_m_snd M \ foldr (*) (map snd M) emp" abbreviation "fi_m_match M \ (\(p,q)\set M. p \\<^sub>A q)" text \A result of the frame matcher. Contains a list of matching pairs, as well as the unmatched parts of P and Q, and the frame F. \ definition [simp]: "FI_RESULT M UP UQ F \ fi_m_match M \ (fi_m_fst M * UP \\<^sub>A fi_m_snd M * UQ * F)" text \Internal structure used by the frame matcher: m contains the matched pairs; p,q the assertions that still needs to be matched; up,uq the assertions that could not be matched; and f the frame. p and q are SLN-delimited syntactic lists. \ definition [simp]: "FI m p q up uq f \ fi_m_match m \ (fi_m_fst m * p * up \\<^sub>A fi_m_snd m * q * uq * f)" text \Initialize processing of query\ lemma FI_init: assumes "FI [] (SLN*P) (SLN*Q) SLN SLN F" shows "FI_QUERY P Q F" using assms by simp text \Construct result from internal representation\ lemma FI_finalize: assumes "FI_RESULT m (p*up) (q*uq) f" shows "FI m p q up uq f" using assms by (simp add: assn_aci) text \Auxiliary lemma to show that all matching pairs together form an entailment. This is required for most applications.\ lemma fi_match_entails: assumes "fi_m_match m" shows "fi_m_fst m \\<^sub>A fi_m_snd m" using assms apply (induct m) apply (simp_all split: prod.split_asm add: ent_star_mono) done text \Internally, the frame matcher tries to match the first assertion of q with the first assertion of p. If no match is found, the first assertion of p is discarded. If no match for any assertion in p can be found, the first assertion of q is discarded.\ text \Match\ lemma FI_match: assumes "p \\<^sub>A q" assumes "FI ((p,q)#m) (ps*up) (qs*uq) SLN SLN f" shows "FI m (ps*p) (qs*q) up uq f" using assms unfolding FI_def by (simp add: assn_aci) text \No match\ lemma FI_p_nomatch: assumes "FI m ps (qs*q) (p*up) uq f" shows "FI m (ps*p) (qs*q) up uq f" using assms unfolding FI_def by (simp add: assn_aci) text \Head of q could not be matched\ lemma FI_q_nomatch: assumes "FI m (SLN*up) qs SLN (q*uq) f" shows "FI m SLN (qs*q) up uq f" using assms unfolding FI_def by (simp add: assn_aci) subsection \Frame Inference\ lemma frame_inference_init: assumes "FI_QUERY P Q F" shows "P \\<^sub>A Q * F" using assms by simp lemma frame_inference_finalize: shows "FI_RESULT M F emp F" apply simp apply rule apply (drule fi_match_entails) apply (rule ent_star_mono[OF _ ent_refl]) apply assumption done subsection \Entailment Solver\ lemma entails_solve_init: "FI_QUERY P Q true \ P \\<^sub>A Q * true" "FI_QUERY P Q emp \ P \\<^sub>A Q" by (simp_all add: assn_aci) lemma entails_solve_finalize: "FI_RESULT M P emp true" "FI_RESULT M emp emp emp" by (auto simp add: fi_match_entails intro: ent_star_mono) lemmas solve_ent_preprocess_simps = ent_pure_post_iff ent_pure_post_iff_sng ent_pure_pre_iff ent_pure_pre_iff_sng subsection \Verification Condition Generator\ lemmas normalize_rules = norm_pre_ex_rule norm_pre_pure_rule (* Originally we introduced backwards-reasoning here, via cons_pre_rule[OF _ return_wp_rule] (old name: complete_return_cons). This only works, if the postcondition is not schematic! However, for forward reasoning, one usually assumes a schematic postcondition! *) text \May be useful in simple, manual proofs, where the postcondition is no schematic variable.\ lemmas return_cons_rule = cons_pre_rule[OF _ return_wp_rule] text \Useful frame-rule variant for manual proof:\ lemma frame_rule_left: "

c \ c <\x. R * Q x>" using frame_rule by (simp add: assn_aci) lemmas deconstruct_rules = bind_rule if_rule false_rule return_sp_rule let_rule case_prod_rule case_list_rule case_option_rule case_sum_rule lemmas heap_rules = ref_rule lookup_rule update_rule new_rule make_rule of_list_rule length_rule nth_rule upd_rule freeze_rule lemma fi_rule: assumes CMD: "

c " assumes FRAME: "Ps \\<^sub>A P * F" shows " c <\x. Q x * F>" apply (rule cons_pre_rule[rotated]) apply (rule frame_rule) apply (rule CMD) apply (rule FRAME) done subsection \ML-setup\ named_theorems sep_dflt_simps "Seplogic: Default simplification rules for automated solvers" named_theorems sep_eintros "Seplogic: Intro rules for entailment solver" named_theorems sep_heap_rules "Seplogic: VCG heap rules" named_theorems sep_decon_rules "Seplogic: VCG deconstruct rules" ML \ infix 1 THEN_IGNORE_NEWGOALS structure Seplogic_Auto = struct (***********************************) (* Tools *) (***********************************) (* Repeat tac on subgoal. Determinize each step. Stop if tac fails or subgoal is solved. *) fun REPEAT_DETERM' tac i st = let val n = Thm.nprems_of st in REPEAT_DETERM (COND (has_fewer_prems n) no_tac (tac i)) st end (***********************************) (* Debugging *) (***********************************) fun tr_term t = Pretty.string_of (Syntax.pretty_term @{context} t); (***********************************) (* Custom Tacticals *) (***********************************) (* Apply tac1, and then tac2 with an offset such that anything left over by tac1 is skipped. The typical usage of this tactic is, if a theorem is instantiated with another theorem that produces additional goals that should be ignored first. Here, it is used in the vcg to ensure that frame inference is done before additional premises (that may depend on the frame) are discharged. *) fun (tac1 THEN_IGNORE_NEWGOALS tac2) i st = let val np = Thm.nprems_of st in (tac1 i THEN (fn st' => let val np' = Thm.nprems_of st' in if np' term) (ts:term list) = let fun frec _ [] = NONE | frec tab (t::ts) = let val k=key_of t in if Termtab.defined tab k then SOME (the (Termtab.lookup tab k),t) else frec (Termtab.update (k,t) tab) ts end in frec Termtab.empty ts end; (* Perform DFS over term with binary operator opN, threading through a state. Atomic terms are transformed by tr. Supports omission of terms from the result structure by transforming them to NONE. *) fun dfs_opr opN (tr:'state -> term -> ('state*term option)) d (t as ((op_t as Const (fN,_))$t1$t2)) = if fN = opN then let val (d1,t1') = dfs_opr opN tr d t1; val (d2,t2') = dfs_opr opN tr d1 t2; in case (t1',t2') of (NONE,NONE) => (d2,NONE) | (SOME t1',NONE) => (d2,SOME t1') | (NONE,SOME t2') => (d2,SOME t2') | (SOME t1',SOME t2') => (d2,SOME (op_t$t1'$t2')) end else tr d t | dfs_opr _ tr d t = tr d t; (* Replace single occurrence of (atomic) ot in t by nt. Returns new term or NONE if nothing was removed. *) fun dfs_replace_atomic opN ot nt t = let fun tr d t = if not d andalso t=ot then (true,SOME nt) else (d,SOME t); val (success,SOME t') = dfs_opr opN tr false t; in if success then SOME t' else NONE end; - fun assn_simproc_fun ctxt credex = let + fun assn_simproc_fun ctxt credex = \<^try>\let val ([redex],ctxt') = Variable.import_terms true [Thm.term_of credex] ctxt; (*val _ = tracing (tr_term redex);*) val export = singleton (Variable.export ctxt' ctxt) fun mk_star t1 t2 = @{term "(*)::assn \ _ \ _"}$t2$t1; fun mk_star' NONE NONE = NONE | mk_star' (SOME t1) NONE = SOME t1 | mk_star' NONE (SOME t2) = SOME t2 | mk_star' (SOME t1) (SOME t2) = SOME (mk_star t1 t2); fun ptrs_key (_$k$_) = k; fun remove_term pt t = case dfs_replace_atomic @{const_name "Groups.times_class.times"} pt @{term emp} t of SOME t' => t'; fun normalize t = let fun ep_tr (has_true,ps,ptrs) t = case t of Const (@{const_name "Assertions.pure_assn"},_)$_ => ((has_true,t::ps,ptrs),NONE) | Const (@{const_name "Assertions.sngr_assn"},_)$_$_ => ((has_true,ps,t::ptrs),SOME t) | Const (@{const_name "Assertions.snga_assn"},_)$_$_ => ((has_true,ps,t::ptrs),SOME t) | Const (@{const_name "Orderings.top_class.top"},_) => ((true,ps,ptrs),NONE) | (inf_op as Const (@{const_name "Lattices.inf_class.inf"},_))$t1$t2 => ((has_true,ps,ptrs),SOME (inf_op$normalize t1$normalize t2)) | _ => ((has_true,ps,ptrs),SOME t); fun normalizer t = case dfs_opr @{const_name "Groups.times_class.times"} ep_tr (false,[],[]) t of ((has_true,ps,ptrs),rt) => ((has_true,rev ps,ptrs),rt); fun normalize_core t = let val ((has_true,pures,ptrs),rt) = normalizer t; val similar = find_similar ptrs_key ptrs; val true_t = if has_true then SOME @{term "Assertions.top_assn"} else NONE; val pures' = case pures of [] => NONE | p::ps => SOME (fold mk_star ps p); in case similar of NONE => the (mk_star' pures' (mk_star' true_t rt)) | SOME (t1,t2) => let val t_stripped = remove_term t1 (remove_term t2 t); in mk_star t_stripped (mk_star t1 t2) end end; fun skip_ex ((exq as Const (@{const_name "ex_assn"},_))$(Abs (n,ty,t))) = exq$Abs (n,ty,skip_ex t) | skip_ex t = normalize_core t; val (bs,t') = strip_abs t; val ty = fastype_of1 (map #2 bs,t'); in if ty = @{typ assn} then Logic.rlist_abs (bs,skip_ex t') else t end; (*val _ = tracing (tr_term redex);*) val (f,terms) = strip_comb redex; val nterms = map (fn t => let (*val _ = tracing (tr_term t); *) val t'=normalize t; (*val _ = tracing (tr_term t');*) in t' end) terms; val new_form = list_comb (f,nterms); val res_ss = (put_simpset HOL_basic_ss ctxt addsimps @{thms star_aci}); val result = Option.map (export o mk_meta_eq) (Arith_Data.prove_conv_nohyps [simp_tac res_ss 1] ctxt' (redex,new_form) ); in result - end handle exc => - if Exn.is_interrupt exc then Exn.reraise exc - else - (tracing ("assn_simproc failed with exception\n:" ^ Runtime.exn_message exc); - NONE) (* Fail silently *); + end catch exc => + (tracing ("assn_simproc failed with exception\n:" ^ Runtime.exn_message exc); + NONE) (* Fail silently *) + \ val assn_simproc = Simplifier.make_simproc @{context} "assn_simproc" {lhss = [@{term "h \ P"}, @{term "P \\<^sub>A Q"}, @{term "P \\<^sub>t Q"}, @{term "Hoare_Triple.hoare_triple P c Q"}, @{term "(P::assn) = Q"}], proc = K assn_simproc_fun}; (***********************************) (* Default Simplifications *) (***********************************) (* Default simplification. MUST contain assertion normalization! Tactic must not fail! *) fun dflt_tac ctxt = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimprocs [assn_simproc] addsimps @{thms norm_assertion_simps} addsimps (Named_Theorems.get ctxt @{named_theorems sep_dflt_simps}) |> fold Splitter.del_split @{thms if_split} ); (***********************************) (* Frame Matcher *) (***********************************) (* Do frame matching imp_solve_tac - tactic used to discharge first assumption of match-rule cf. lemma FI_match. *) fun match_frame_tac imp_solve_tac ctxt = let (* Normalize star-lists *) val norm_tac = simp_tac ( put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_normalize}); (* Strip star-lists *) val strip_tac = simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_strip}) THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_def}); (* Do a match step *) val match_tac = resolve_tac ctxt @{thms FI_match} (* Separate p,q*) THEN' SOLVED' imp_solve_tac (* Solve implication *) THEN' norm_tac; (* Do a no-match step *) val nomatch_tac = resolve_tac ctxt @{thms FI_p_nomatch} ORELSE' (resolve_tac ctxt @{thms FI_q_nomatch} THEN' norm_tac); in resolve_tac ctxt @{thms FI_init} THEN' norm_tac THEN' REPEAT_DETERM' (FIRST' [ CHANGED o dflt_tac ctxt, (match_tac ORELSE' nomatch_tac)]) THEN' resolve_tac ctxt @{thms FI_finalize} THEN' strip_tac end; (***********************************) (* Frame Inference *) (***********************************) fun frame_inference_tac ctxt = resolve_tac ctxt @{thms frame_inference_init} THEN' match_frame_tac (resolve_tac ctxt @{thms ent_refl}) ctxt THEN' resolve_tac ctxt @{thms frame_inference_finalize}; (***********************************) (* Entailment Solver *) (***********************************) (* Extract existential quantifiers from entailment goal *) fun extract_ex_tac ctxt i st = let fun count_ex (Const (@{const_name Assertions.entails},_)$_$c) = count_ex c RS @{thm HOL.mp} | count_ex (Const (@{const_name Assertions.ex_assn},_)$Abs (_,_,t)) = count_ex t RS @{thm enorm_exI'} | count_ex _ = @{thm imp_refl}; val concl = Logic.concl_of_goal (Thm.prop_of st) i |> HOLogic.dest_Trueprop; val thm = count_ex concl; in (TRY o REPEAT_ALL_NEW (match_tac ctxt @{thms ent_ex_preI}) THEN' resolve_tac ctxt [thm]) i st end; (* Solve Entailment *) fun solve_entails_tac ctxt = let val preprocess_entails_tac = dflt_tac ctxt THEN' extract_ex_tac ctxt THEN' simp_tac (put_simpset HOL_ss ctxt addsimps @{thms solve_ent_preprocess_simps}); val match_entails_tac = resolve_tac ctxt @{thms entails_solve_init} THEN' match_frame_tac (resolve_tac ctxt @{thms ent_refl}) ctxt THEN' resolve_tac ctxt @{thms entails_solve_finalize}; in preprocess_entails_tac THEN' (TRY o REPEAT_ALL_NEW (match_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems sep_eintros})))) THEN_ALL_NEW (dflt_tac ctxt THEN' TRY o (match_tac ctxt @{thms ent_triv} ORELSE' resolve_tac ctxt @{thms ent_refl} ORELSE' match_entails_tac)) end; (***********************************) (* Verification Condition Generator*) (***********************************) fun heap_rule_tac ctxt h_thms = resolve_tac ctxt h_thms ORELSE' ( resolve_tac ctxt @{thms fi_rule} THEN' (resolve_tac ctxt h_thms THEN_IGNORE_NEWGOALS frame_inference_tac ctxt)); fun vcg_step_tac ctxt = let val h_thms = rev (Named_Theorems.get ctxt @{named_theorems sep_heap_rules}); val d_thms = rev (Named_Theorems.get ctxt @{named_theorems sep_decon_rules}); val heap_rule_tac = heap_rule_tac ctxt h_thms (* Apply consequence rule if postcondition is not a schematic var *) fun app_post_cons_tac i st = case Logic.concl_of_goal (Thm.prop_of st) i |> HOLogic.dest_Trueprop of Const (@{const_name Hoare_Triple.hoare_triple},_)$_$_$qt => if is_Var (head_of qt) then no_tac st else resolve_tac ctxt @{thms cons_post_rule} i st | _ => no_tac st; in CSUBGOAL (snd #> (FIRST' [ CHANGED o dflt_tac ctxt, REPEAT_ALL_NEW (resolve_tac ctxt @{thms normalize_rules}), CHANGED o (FIRST' [resolve_tac ctxt d_thms, heap_rule_tac] ORELSE' (app_post_cons_tac THEN' FIRST' [resolve_tac ctxt d_thms, heap_rule_tac])) ])) end; fun vcg_tac ctxt = REPEAT_DETERM' (vcg_step_tac ctxt) (***********************************) (* Automatic Solver *) (***********************************) fun sep_autosolve_tac do_pre do_post ctxt = let val pre_tacs = [ CHANGED o clarsimp_tac ctxt, CHANGED o REPEAT_ALL_NEW (match_tac ctxt @{thms ballI allI impI conjI}) ]; val main_tacs = [ match_tac ctxt @{thms is_hoare_triple} THEN' CHANGED o vcg_tac ctxt, match_tac ctxt @{thms is_entails} THEN' CHANGED o solve_entails_tac ctxt ]; val post_tacs = [SELECT_GOAL (auto_tac ctxt)]; val tacs = (if do_pre then pre_tacs else []) @ main_tacs @ (if do_post then post_tacs else []); in REPEAT_DETERM' (CHANGED o FIRST' tacs) end; (***********************************) (* Method Setup *) (***********************************) val dflt_simps_modifiers = [ Args.$$$ "dflt_simps" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_dflt_simps}) \<^here>), Args.$$$ "dflt_simps" -- Scan.option Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_dflt_simps}) \<^here>) ]; val heap_modifiers = [ Args.$$$ "heap" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_heap_rules}) \<^here>), Args.$$$ "heap" -- Scan.option Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_heap_rules}) \<^here>) ]; val decon_modifiers = [ Args.$$$ "decon" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_decon_rules}) \<^here>), Args.$$$ "decon" -- Scan.option Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_decon_rules}) \<^here>) ]; val eintros_modifiers = [ Args.$$$ "eintros" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_eintros}) \<^here>), Args.$$$ "eintros" -- Scan.option Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_eintros}) \<^here>) ]; val solve_entails_modifiers = dflt_simps_modifiers @ eintros_modifiers; val vcg_modifiers = heap_modifiers @ decon_modifiers @ dflt_simps_modifiers; val sep_auto_modifiers = clasimp_modifiers @ vcg_modifiers @ eintros_modifiers; end; \ simproc_setup assn_simproc ("h\P" | "P\\<^sub>AQ" | "P\\<^sub>tQ" | "

c " | "(P::assn) = Q") = \K Seplogic_Auto.assn_simproc_fun\ method_setup assn_simp =\Scan.succeed (fn ctxt => (SIMPLE_METHOD' ( CHANGED o Seplogic_Auto.dflt_tac ctxt )))\ "Seplogic: Simplification of assertions" method_setup frame_inference = \Scan.succeed (fn ctxt => (SIMPLE_METHOD' ( CHANGED o Seplogic_Auto.frame_inference_tac ctxt )))\ "Seplogic: Frame inference" method_setup solve_entails = \ Method.sections Seplogic_Auto.solve_entails_modifiers >> (fn _ => fn ctxt => SIMPLE_METHOD' ( CHANGED o Seplogic_Auto.solve_entails_tac ctxt ))\ "Seplogic: Entailment Solver" method_setup heap_rule = \ Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' ( let val thms = case thms of [] => rev (Named_Theorems.get ctxt @{named_theorems sep_heap_rules}) | _ => thms in CHANGED o Seplogic_Auto.heap_rule_tac ctxt thms end ))\ "Seplogic: Apply rule with frame inference" method_setup vcg = \ Scan.lift (Args.mode "ss") -- Method.sections Seplogic_Auto.vcg_modifiers >> (fn (ss,_) => fn ctxt => SIMPLE_METHOD' ( CHANGED o ( if ss then Seplogic_Auto.vcg_step_tac ctxt else Seplogic_Auto.vcg_tac ctxt ) ))\ "Seplogic: Verification Condition Generator" method_setup sep_auto = \Scan.lift (Args.mode "nopre" -- Args.mode "nopost" -- Args.mode "plain") --| Method.sections Seplogic_Auto.sep_auto_modifiers >> (fn ((nopre,nopost),plain) => fn ctxt => SIMPLE_METHOD' ( CHANGED o Seplogic_Auto.sep_autosolve_tac ((not nopre) andalso (not plain)) ((not nopost) andalso (not plain)) ctxt ))\ "Seplogic: Automatic solver" lemmas [sep_dflt_simps] = split declare deconstruct_rules[sep_decon_rules] declare heap_rules[sep_heap_rules] lemmas [sep_eintros] = impI conjI exI subsection \Semi-Automatic Reasoning\ text \In this section, we provide some lemmas for semi-automatic reasoning\ text \Forward reasoning with frame. Use \frame_inference\-method to discharge second assumption.\ lemma ent_frame_fwd: assumes R: "P \\<^sub>A R" assumes F: "Ps \\<^sub>A P*F" assumes I: "R*F \\<^sub>A Q" shows "Ps \\<^sub>A Q" using assms by (metis ent_refl ent_star_mono ent_trans) lemma mod_frame_fwd: assumes M: "h\Ps" assumes R: "P\\<^sub>AR" assumes F: "Ps \\<^sub>A P*F" shows "h\R*F" using assms by (metis ent_star_mono entails_def) text \Apply precision rule with frame inference.\ lemma prec_frame: assumes PREC: "precise P" assumes M1: "h\(R1 \\<^sub>A R2)" assumes F1: "R1 \\<^sub>A P x p * F1" assumes F2: "R2 \\<^sub>A P y p * F2" shows "x=y" using preciseD[OF PREC] M1 F1 F2 by (metis entailsD mod_and_dist) lemma prec_frame_expl: assumes PREC: "\x y. (h\(P x * F1) \\<^sub>A (P y * F2)) \ x=y" assumes M1: "h\(R1 \\<^sub>A R2)" assumes F1: "R1 \\<^sub>A P x * F1" assumes F2: "R2 \\<^sub>A P y * F2" shows "x=y" using assms by (metis entailsD mod_and_dist) text \Variant that is useful within induction proofs, where induction goes over \x\ or \y\\ lemma prec_frame': assumes PREC: "(h\(P x * F1) \\<^sub>A (P y * F2)) \ x=y" assumes M1: "h\(R1 \\<^sub>A R2)" assumes F1: "R1 \\<^sub>A P x * F1" assumes F2: "R2 \\<^sub>A P y * F2" shows "x=y" using assms by (metis entailsD mod_and_dist) lemma ent_wand_frameI: assumes "(Q -* R) * F \\<^sub>A S" assumes "P \\<^sub>A F * X" assumes "Q*X \\<^sub>A R" shows "P \\<^sub>A S" using assms by (metis ent_frame_fwd ent_wandI mult.commute) subsubsection \Manual Frame Inference\ lemma ent_true_drop: "P\\<^sub>AQ*true \ P*R\\<^sub>AQ*true" "P\\<^sub>AQ \ P\\<^sub>AQ*true" apply (metis assn_times_comm ent_star_mono ent_true merge_true_star_ctx) apply (metis assn_one_left ent_star_mono ent_true star_aci(2)) done lemma fr_refl: "A\\<^sub>AB \ A*C \\<^sub>AB*C" by (blast intro: ent_star_mono ent_refl) lemma fr_rot: "(A*B \\<^sub>A C) \ (B*A \\<^sub>A C)" by (simp add: assn_aci) lemma fr_rot_rhs: "(A \\<^sub>A B*C) \ (A \\<^sub>A C*B)" by (simp add: assn_aci) lemma ent_star_mono_true: assumes "A \\<^sub>A A' * true" assumes "B \\<^sub>A B' * true" shows "A*B*true \\<^sub>A A'*B'*true" using ent_star_mono[OF assms] apply simp using ent_true_drop(1) by blast lemma ent_refl_true: "A \\<^sub>A A * true" by (simp add: ent_true_drop(2)) lemma entt_fr_refl: "F\\<^sub>tF' \ F*A \\<^sub>t F'*A" by (rule entt_star_mono) auto lemma entt_fr_drop: "F\\<^sub>tF' \ F*A \\<^sub>t F'" using ent_true_drop(1) enttD enttI by blast method_setup fr_rot = \ let fun rot_tac ctxt = resolve_tac ctxt @{thms fr_rot} THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms star_assoc[symmetric]}) in Scan.lift Parse.nat >> (fn n => fn ctxt => SIMPLE_METHOD' ( fn i => REPEAT_DETERM_N n (rot_tac ctxt i))) end \ method_setup fr_rot_rhs = \ let fun rot_tac ctxt = resolve_tac ctxt @{thms fr_rot_rhs} THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms star_assoc[symmetric]}) in Scan.lift Parse.nat >> (fn n => fn ctxt => SIMPLE_METHOD' ( fn i => REPEAT_DETERM_N n (rot_tac ctxt i))) end \ (*<*) subsection \Test Cases\ lemma "\x. A x * true * Q x \\<^sub>A true * A x * Q x" apply simp done lemma "A * (true * B) \\<^sub>A true * A * B" apply (simp) done lemma "h\true*P*true \ h\P*true" by simp lemma "A * true * \(b \ c) * true * B \\<^sub>A \b * \c * true *A * B" by simp lemma "\y c. \\<^sub>Ax. P x * (R x * Q y) * \ (b \ c) \\<^sub>A (\\<^sub>Ax. \b * (P x * (R x * Q y) * \c))" apply simp done lemma "A * B * (\c * B * C * D * \a * true * \d) * (\\<^sub>Ax. E x * F * \b) * true \\<^sub>A (\\<^sub>Ax. \ (c \ a \ d \ b) * true * A * B * (true * B * C * D) * (E x * F))" apply simp done lemma "

c <\r. Q r * true * \(b r) * true * \a> \

c <\r. Q r * true * \(b r \ a)>" apply simp done lemma "(h\((A*B*\b*true*\c*true) \\<^sub>A (\(p=q)*P*Q))) \ h \ A * B * true \\<^sub>A P * Q \ b \ c \ p = q" apply simp done lemma assumes "FI_RESULT [(B, B), (A, A)] C D F" shows "FI_QUERY (A*B*C) (D*B*A) F" apply (tactic \Seplogic_Auto.match_frame_tac (resolve_tac @{context} @{thms ent_refl}) @{context} 1\) by (rule assms) lemma assumes "FI_RESULT [(B,B), (A,A)] C emp F" shows "FI_QUERY (A*B*C) (B*A) F" apply (tactic \Seplogic_Auto.match_frame_tac (resolve_tac @{context} @{thms ent_refl}) @{context} 1\) by (rule assms) lemma assumes "FI_RESULT [(B, B), (A, A)] emp emp F" shows "FI_QUERY (A*B) (B*A) F" apply (tactic \Seplogic_Auto.match_frame_tac (resolve_tac @{context} @{thms ent_refl}) @{context} 1\) by (rule assms) lemma assumes "FI_RESULT [(A, A)] emp emp F" shows "FI_QUERY (A) (A) F" apply (tactic \Seplogic_Auto.match_frame_tac (resolve_tac @{context} @{thms ent_refl}) @{context} 1\) by (rule assms) lemma assumes "FI_RESULT [(A, A)] (B * C * D) emp F" shows "FI_QUERY (B*C*D*A) (A) F" apply (tactic \Seplogic_Auto.match_frame_tac (resolve_tac @{context} @{thms ent_refl}) @{context} 1\) by (rule assms) schematic_goal "P1 * P2 * P3 * P4 \\<^sub>A P3 * ?R1" "P1 * (P2 * (P3 * P4)) \\<^sub>A P1 * ?R2" "P4 * (P2 * (P1 * P3)) \\<^sub>A P1 * ?R2'" "P1 * P2 * P3 * P4 \\<^sub>A P4 * ?R3" "P1 * P2 \\<^sub>A P1 * ?R4" "P1 * P2 \\<^sub>A P2 * ?R5" "P1 \\<^sub>A P1 * ?R6" "P1 * P2 \\<^sub>A emp * ?R7" by frame_inference+ lemma "\A; B; C; b 17\ \ Q 1 5 3 \\<^sub>A (\\<^sub>Ax y z. \\<^sub>Aa. Q x y z * \(b a) * \(y=5))" by solve_entails thm nth_rule lemma "

\<^sub>a[1,2,3]> do { v\Array.nth x 1; return v } <\r. P * x\\<^sub>a[1,2,3] * \(r=2)>" apply sep_auto done (*>*) subsection \Quick Overview of Proof Methods\ text_raw \\label{sec:auto:overview}\ text \ In this section, we give a quick overview of the available proof methods and options. The most versatile proof method that we provide is \sep_auto\. It tries to solve the first subgoal, invoking appropriate proof methods as required. If it cannot solve the subgoal completely, it stops at the intermediate state that it could not handle any more. \sep_auto\ can be configured by section-arguments for the simplifier, the classical reasoner, and all section-arguments for the verification condition generator and entailment solver. Moreover, it takes an optional mode argument (mode), where valid modes are: \begin{description} \item[(nopre)] No preprocessing of goal. The preprocessor tries to clarify and simplify the goal before the main method is invoked. \item[(nopost)] No postprocessing of goal. The postprocessor tries to solve or simplify goals left over by verification condition generation or entailment solving. \item[(plain)] Neither pre- nor postprocessing. Just applies vcg and entailment solver. \end{description} \paragraph{Entailment Solver.} The entailment solver processes goals of the form \P \\<^sub>A Q\. It is invoked by the method \solve_entails\. It first tries to pull out pure parts of \P\ and \Q\. This may introduce quantifiers, conjunction, and implication into the goal, that are eliminated by resolving with rules declared as \sep_eintros\ (method argument: eintros[add/del]:). Moreover, it simplifies with rules declared as \sep_dflt_simps\ (section argument: \dflt_simps[add/del]:\). Now, \P\ and \Q\ should have the form \X\<^sub>1*\*X\<^sub>n\. Then, the frame-matcher is used to match all items of \P\ with items of \Q\, and thus solve the implication. Matching is currently done syntactically, but can instantiate schematic variables. Note that, by default, existential introduction is declared as \sep_eintros\-rule. This introduces schematic variables, that can later be matched against. However, in some cases, the matching may instantiate the schematic variables in an undesired way. In this case, the argument \eintros del: exI\ should be passed to the entailment solver, and the existential quantifier should be instantiated manually. \paragraph{Frame Inference} The method \frame_inference\ tries to solve a goal of the form \P\Q*?F\, by matching \Q\ against the parts of \P\, and instantiating \?F\ accordingly. Matching is done syntactically, possibly instantiating schematic variables. \P\ and \Q\ should be assertions separated by \*\. Note that frame inference does no simplification or other kinds of normalization. The method \heap_rule\ applies the specified heap rules, using frame inference if necessary. If no rules are specified, the default heap rules are used. \paragraph{Verification Condition Generator} The verification condition generator processes goals of the form \

c\. It is invoked by the method \vcg\. First, it tries to pull out pure parts and simplifies with the default simplification rules. Then, it tries to resolve the goal with deconstruct rules (attribute: \sep_decon_rules\, section argument: \decon[add/del]:\), and if this does not succeed, it tries to resolve the goal with heap rules (attribute: \sep_heap_rules\, section argument: \heap[add/del]:\), using the frame rule and frame inference. If resolving is not possible, it also tries to apply the consequence rule to make the postcondition a schematic variable. \ (*<*) subsection \Hiding of internal stuff\ hide_const (open) FI SLN (*>*) end diff --git a/thys/SpecCheck/property.ML b/thys/SpecCheck/property.ML --- a/thys/SpecCheck/property.ML +++ b/thys/SpecCheck/property.ML @@ -1,54 +1,50 @@ (* Title: SpecCheck/property.ML Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen Author: Christopher League The base module of testable properties. A property is the type of values that SpecCheck knows how to test. Properties not only test whether a given predicate holds, but, for example, can also have preconditions. *) signature SPECCHECK_PROPERTY = sig type 'a pred = 'a -> bool (*the type of values testable by SpecCheck*) type 'a prop (*transforms a predicate into a testable property*) val prop : 'a pred -> 'a prop (*implication for properties: if the first argument evaluates to false, the test case is discarded*) val implies : 'a pred -> 'a prop -> 'a prop (*convenient notation for `implies` working on predicates*) val ==> : 'a pred * 'a pred -> 'a prop val expect_failure : exn -> ('a -> 'b) -> 'a prop end structure SpecCheck_Property : SPECCHECK_PROPERTY = struct type 'a pred = 'a -> bool type 'a prop = 'a -> SpecCheck_Base.result_single -fun apply f x = SpecCheck_Base.Result (f x) - (*testcode may throw arbitrary exceptions; interrupts must not be caught!*) - handle exn => if Exn.is_interrupt exn then Exn.reraise exn else SpecCheck_Base.Exception exn +fun apply f x = \<^try>\SpecCheck_Base.Result (f x) catch exn => SpecCheck_Base.Exception exn\ fun prop f x = apply f x fun implies cond prop x = if cond x then prop x else SpecCheck_Base.Discard fun ==> (p1, p2) = implies p1 (prop p2) fun eq_exn (exn, exn') = exnName exn = exnName exn' andalso exnMessage exn = exnMessage exn' fun expect_failure exp_exn f = prop (fn x => - (f x; false) - handle exn => if Exn.is_interrupt exn then Exn.reraise exn else eq_exn (exn, exp_exn) - ) + \<^try>\(f x; false) catch exn => eq_exn (exn, exp_exn)\) end diff --git a/thys/Van_Emde_Boas_Trees/Separation_Logic_Imperative_HOL/Automation.thy b/thys/Van_Emde_Boas_Trees/Separation_Logic_Imperative_HOL/Automation.thy --- a/thys/Van_Emde_Boas_Trees/Separation_Logic_Imperative_HOL/Automation.thy +++ b/thys/Van_Emde_Boas_Trees/Separation_Logic_Imperative_HOL/Automation.thy @@ -1,1071 +1,1070 @@ section \Automation\ theory Automation imports Hoare_Triple Refine_Imp_Hol (*"../Lib/Refine_Util"*) begin text \ In this theory, we provide a set of tactics and a simplifier setup for easy reasoning with our separation logic.\ subsection \Normalization of Assertions\ text \ In this section, we provide a set of lemmas and a simplifier setup to bring assertions to a normal form. We provide a simproc that detects pure parts of assertions and duplicate pointers. Moreover, we provide ac-rules for assertions. See Section~\ref{sec:auto:overview} for a short overview of the available proof methods. \ lemmas assn_aci = inf_aci[where 'a=assn] sup_aci[where 'a=assn] mult.left_ac[where 'a=assn] lemmas star_assoc = mult.assoc[where 'a=assn] lemmas assn_assoc = mult.left_assoc inf_assoc[where 'a=assn] sup_assoc[where 'a=assn] lemma merge_true_star_ctx: "true * (true * P) = true * P" by (simp add: mult.left_ac) lemmas star_aci = mult.assoc[where 'a=assn] mult.commute[where 'a=assn] mult.left_commute[where 'a=assn] assn_one_left mult_1_right[where 'a=assn] merge_true_star merge_true_star_ctx text \Move existential quantifiers to the front of assertions\ lemma ex_assn_move_out[simp]: "\Q R. (\\<^sub>Ax. Q x) * R = (\\<^sub>Ax. (Q x * R))" "\Q R. R * (\\<^sub>Ax. Q x) = (\\<^sub>Ax. (R * Q x))" "\P Q. (\\<^sub>Ax. Q x) \\<^sub>A P = (\\<^sub>Ax. (Q x \\<^sub>A P)) " "\P Q. Q \\<^sub>A (\\<^sub>Ax. P x) = (\\<^sub>Ax. (Q \\<^sub>A P x))" "\P Q. (\\<^sub>Ax. Q x) \\<^sub>A P = (\\<^sub>Ax. (Q x \\<^sub>A P))" "\P Q. Q \\<^sub>A (\\<^sub>Ax. P x) = (\\<^sub>Ax. (Q \\<^sub>A P x))" apply - apply (simp add: ex_distrib_star) apply (subst mult.commute) apply (subst (2) mult.commute) apply (simp add: ex_distrib_star) apply (simp add: ex_distrib_and) apply (subst inf_commute) apply (subst (2) inf_commute) apply (simp add: ex_distrib_and) apply (simp add: ex_distrib_or) apply (subst sup_commute) apply (subst (2) sup_commute) apply (simp add: ex_distrib_or) done text \Extract pure assertions from and-clauses\ lemma and_extract_pure_left_iff[simp]: "\b \\<^sub>A Q = (emp\\<^sub>AQ)*\b" by (cases b) auto lemma and_extract_pure_left_ctx_iff[simp]: "P*\b \\<^sub>A Q = (P\\<^sub>AQ)*\b" by (cases b) auto lemma and_extract_pure_right_iff[simp]: "P \\<^sub>A \b = (emp\\<^sub>AP)*\b" by (cases b) (auto simp: assn_aci) lemma and_extract_pure_right_ctx_iff[simp]: "P \\<^sub>A Q*\b = (P\\<^sub>AQ)*\b" by (cases b) auto lemmas and_extract_pure_iff = and_extract_pure_left_iff and_extract_pure_left_ctx_iff and_extract_pure_right_iff and_extract_pure_right_ctx_iff lemmas norm_assertion_simps = (* Neutral elements *) mult_1[where 'a=assn] mult_1_right[where 'a=assn] inf_top_left[where 'a=assn] inf_top_right[where 'a=assn] sup_bot_left[where 'a=assn] sup_bot_right[where 'a=assn] (* Zero elements *) star_false_left star_false_right inf_bot_left[where 'a=assn] inf_bot_right[where 'a=assn] sup_top_left[where 'a=assn] sup_top_right[where 'a=assn] (* Associativity *) mult.left_assoc[where 'a=assn] inf_assoc[where 'a=assn] sup_assoc[where 'a=assn] (* Existential Quantifiers *) ex_assn_move_out ex_assn_const (* Extract pure assertions from conjunctions *) and_extract_pure_iff (* Merging *) merge_pure_star merge_pure_and merge_pure_or merge_true_star inf_idem[where 'a=assn] sup_idem[where 'a=assn] (* Duplicated References *) sngr_same_false snga_same_false subsubsection \Simplifier Setup Fine-Tuning\ (*text \Imperative HOL likes to simplify pointer inequations to this strange operator. We do some additional simplifier setup here\ lemma not_same_noteqr[simp]: "\ a=!=a" by (metis Ref.unequal) declare Ref.noteq_irrefl[dest!] lemma not_same_noteqa[simp]: "\ a=!!=a" by (metis Array.unequal) declare Array.noteq_irrefl[dest!] *) text \However, it is safest to disable this rewriting, as there is a working standard simplifier setup for \(\)\ \ (*declare Ref.unequal[simp del] declare Array.unequal[simp del] *) subsection \Normalization of Entailments\ text \Used by existential quantifier extraction tactic\ lemma enorm_exI': (* Incomplete, as chosen x may depend on heap! *) "(\x. Z x \ (P \\<^sub>A Q x)) \ (\x. Z x) \ (P \\<^sub>A (\\<^sub>Ax. Q x))" by (metis ent_ex_postI) text \Example of how to build an extraction lemma.\ thm enorm_exI'[OF enorm_exI'[OF imp_refl]] lemmas ent_triv = ent_true ent_false text \Dummy rule to detect Hoare triple goal\ lemma is_hoare_triple: "

c \

c " . text \Dummy rule to detect entailment goal\ lemma is_entails: "P\\<^sub>AQ \ P \\<^sub>AQ" . subsection \Frame Matcher\ text \Given star-lists P,Q and a frame F, this method tries to match all elements of Q with corresponding elements of P. The result is a partial match, that contains matching pairs and the unmatched content.\ text \The frame-matcher internally uses syntactic lists separated by star, and delimited by the special symbol \SLN\, which is defined to be \emp\.\ definition [simp]: "SLN \ emp" lemma SLN_left: "SLN * P = P" by simp lemma SLN_right: "P * SLN = P" by simp lemmas SLN_normalize = SLN_right mult.left_assoc[where 'a=assn] lemmas SLN_strip = SLN_right SLN_left mult.left_assoc[where 'a=assn] text \A query to the frame matcher. Contains the assertions P and Q that shall be matched, as well as a frame F, that is not touched.\ definition [simp]: "FI_QUERY P Q F \ P \\<^sub>A Q*F" abbreviation "fi_m_fst M \ foldr (*) (map fst M) emp" abbreviation "fi_m_snd M \ foldr (*) (map snd M) emp" abbreviation "fi_m_match M \ (\(p,q)\set M. p \\<^sub>A q)" text \A result of the frame matcher. Contains a list of matching pairs, as well as the unmatched parts of P and Q, and the frame F. \ definition [simp]: "FI_RESULT M UP UQ F \ fi_m_match M \ (fi_m_fst M * UP \\<^sub>A fi_m_snd M * UQ * F)" text \Internal structure used by the frame matcher: m contains the matched pairs; p,q the assertions that still needs to be matched; up,uq the assertions that could not be matched; and f the frame. p and q are SLN-delimited syntactic lists. \ definition [simp]: "FI m p q up uq f \ fi_m_match m \ (fi_m_fst m * p * up \\<^sub>A fi_m_snd m * q * uq * f)" text \Initialize processing of query\ lemma FI_init: assumes "FI [] (SLN*P) (SLN*Q) SLN SLN F" shows "FI_QUERY P Q F" using assms by simp text \Construct result from internal representation\ lemma FI_finalize: assumes "FI_RESULT m (p*up) (q*uq) f" shows "FI m p q up uq f" using assms by (simp add: assn_aci) text \Auxiliary lemma to show that all matching pairs together form an entailment. This is required for most applications.\ lemma fi_match_entails: assumes "fi_m_match m" shows "fi_m_fst m \\<^sub>A fi_m_snd m" using assms apply (induct m) apply (simp_all split: prod.split_asm add: ent_star_mono) done text \Internally, the frame matcher tries to match the first assertion of q with the first assertion of p. If no match is found, the first assertion of p is discarded. If no match for any assertion in p can be found, the first assertion of q is discarded.\ text \Match\ lemma FI_match: assumes "p \\<^sub>A q" assumes "FI ((p,q)#m) (ps*up) (qs*uq) SLN SLN f" shows "FI m (ps*p) (qs*q) up uq f" using assms unfolding FI_def by (simp add: assn_aci) text \No match\ lemma FI_p_nomatch: assumes "FI m ps (qs*q) (p*up) uq f" shows "FI m (ps*p) (qs*q) up uq f" using assms unfolding FI_def by (simp add: assn_aci) text \Head of q could not be matched\ lemma FI_q_nomatch: assumes "FI m (SLN*up) qs SLN (q*uq) f" shows "FI m SLN (qs*q) up uq f" using assms unfolding FI_def by (simp add: assn_aci) subsection \Frame Inference\ lemma frame_inference_init: assumes "FI_QUERY P Q F" shows "P \\<^sub>A Q * F" using assms by simp lemma frame_inference_finalize: shows "FI_RESULT M F emp F" apply simp apply rule apply (drule fi_match_entails) apply (rule ent_star_mono[OF _ ent_refl]) apply assumption done subsection \Entailment Solver\ lemma entails_solve_init: "FI_QUERY P Q true \ P \\<^sub>A Q * true" "FI_QUERY P Q emp \ P \\<^sub>A Q" by (simp_all add: assn_aci) lemma entails_solve_finalize: "FI_RESULT M P emp true" "FI_RESULT M emp emp emp" by (auto simp add: fi_match_entails intro: ent_star_mono) lemmas solve_ent_preprocess_simps = ent_pure_post_iff ent_pure_post_iff_sng ent_pure_pre_iff ent_pure_pre_iff_sng subsection \Verification Condition Generator\ lemmas normalize_rules = norm_pre_ex_rule norm_pre_pure_rule (* Originally we introduced backwards-reasoning here, via cons_pre_rule[OF _ return_wp_rule] (old name: complete_return_cons). This only works, if the postcondition is not schematic! However, for forward reasoning, one usually assumes a schematic postcondition! *) text \May be useful in simple, manual proofs, where the postcondition is no schematic variable.\ lemmas return_cons_rule = cons_pre_rule[OF _ return_wp_rule] text \Useful frame-rule variant for manual proof:\ lemma frame_rule_left: "

c \ c <\x. R * Q x>" using frame_rule by (simp add: assn_aci) lemmas deconstruct_rules = wait_bind_decon assert'_bind_rule bind_rule if_rule false_rule return_sp_rule let_rule case_prod_rule case_list_rule case_option_rule case_sum_rule lemmas heap_rules = ref_rule lookup_rule update_rule new_rule make_rule of_list_rule length_rule nth_rule upd_rule freeze_rule wait_rule assert'_rule lemma fi_rule: assumes CMD: "

c " assumes FRAME: "Ps \\<^sub>A P * F" shows " c <\x. Q x * F>" apply (rule cons_pre_rule[rotated]) apply (rule frame_rule) apply (rule CMD) apply (rule FRAME) done subsection \ML-setup\ named_theorems sep_dflt_simps "Seplogic: Default simplification rules for automated solvers" named_theorems sep_eintros "Seplogic: Intro rules for entailment solver" named_theorems sep_heap_rules "Seplogic: VCG heap rules" named_theorems sep_decon_rules "Seplogic: VCG deconstruct rules" ML \ infix 1 THEN_IGNORE_NEWGOALS structure Seplogic_Auto = struct (***********************************) (* Tools *) (***********************************) (* Repeat tac on subgoal. Determinize each step. Stop if tac fails or subgoal is solved. *) fun REPEAT_DETERM' tac i st = let val n = Thm.nprems_of st in REPEAT_DETERM (COND (has_fewer_prems n) no_tac (tac i)) st end (***********************************) (* Debugging *) (***********************************) fun tr_term t = Pretty.string_of (Syntax.pretty_term @{context} t); (***********************************) (* Custom Tacticals *) (***********************************) (* Apply tac1, and then tac2 with an offset such that anything left over by tac1 is skipped. The typical usage of this tactic is, if a theorem is instantiated with another theorem that produces additional goals that should be ignored first. Here, it is used in the vcg to ensure that frame inference is done before additional premises (that may depend on the frame) are discharged. *) fun (tac1 THEN_IGNORE_NEWGOALS tac2) i st = let val np = Thm.nprems_of st in (tac1 i THEN (fn st' => let val np' = Thm.nprems_of st' in if np' term) (ts:term list) = let fun frec _ [] = NONE | frec tab (t::ts) = let val k=key_of t in if Termtab.defined tab k then SOME (the (Termtab.lookup tab k),t) else frec (Termtab.update (k,t) tab) ts end in frec Termtab.empty ts end; (* Perform DFS over term with binary operator opN, threading through a state. Atomic terms are transformed by tr. Supports omission of terms from the result structure by transforming them to NONE. *) fun dfs_opr opN (tr:'state -> term -> ('state*term option)) d (t as ((op_t as Const (fN,_))$t1$t2)) = if fN = opN then let val (d1,t1') = dfs_opr opN tr d t1; val (d2,t2') = dfs_opr opN tr d1 t2; in case (t1',t2') of (NONE,NONE) => (d2,NONE) | (SOME t1',NONE) => (d2,SOME t1') | (NONE,SOME t2') => (d2,SOME t2') | (SOME t1',SOME t2') => (d2,SOME (op_t$t1'$t2')) end else tr d t | dfs_opr _ tr d t = tr d t; (* Replace single occurrence of (atomic) ot in t by nt. Returns new term or NONE if nothing was removed. *) fun dfs_replace_atomic opN ot nt t = let fun tr d t = if not d andalso t=ot then (true,SOME nt) else (d,SOME t); val (success,SOME t') = dfs_opr opN tr false t; in if success then SOME t' else NONE end; - fun assn_simproc_fun ctxt credex = let + fun assn_simproc_fun ctxt credex = \<^try>\let val ([redex],ctxt') = Variable.import_terms true [Thm.term_of credex] ctxt; (*val _ = tracing (tr_term redex);*) val export = singleton (Variable.export ctxt' ctxt) fun mk_star t1 t2 = @{term "(*)::assn \ _ \ _"}$t2$t1; fun mk_star' NONE NONE = NONE | mk_star' (SOME t1) NONE = SOME t1 | mk_star' NONE (SOME t2) = SOME t2 | mk_star' (SOME t1) (SOME t2) = SOME (mk_star t1 t2); fun ptrs_key (_$k$_) = k; fun remove_term pt t = case dfs_replace_atomic @{const_name "Groups.times_class.times"} pt @{term emp} t of SOME t' => t'; fun normalize t = let fun ep_tr (has_true,ps,ptrs) t = case t of Const (@{const_name "Assertions.pure_assn"},_)$_ => ((has_true,t::ps,ptrs),NONE) | Const (@{const_name "Assertions.sngr_assn"},_)$_$_ => ((has_true,ps,t::ptrs),SOME t) | Const (@{const_name "Assertions.snga_assn"},_)$_$_ => ((has_true,ps,t::ptrs),SOME t) | Const (@{const_name "Orderings.top_class.top"},_) => ((true,ps,ptrs),NONE) | (inf_op as Const (@{const_name "Lattices.inf_class.inf"},_))$t1$t2 => ((has_true,ps,ptrs),SOME (inf_op$normalize t1$normalize t2)) | _ => ((has_true,ps,ptrs),SOME t); fun normalizer t = case dfs_opr @{const_name "Groups.times_class.times"} ep_tr (false,[],[]) t of ((has_true,ps,ptrs),rt) => ((has_true,rev ps,ptrs),rt); fun normalize_core t = let val ((has_true,pures,ptrs),rt) = normalizer t; val similar = find_similar ptrs_key ptrs; val true_t = if has_true then SOME @{term "Assertions.top_assn"} else NONE; val pures' = case pures of [] => NONE | p::ps => SOME (fold mk_star ps p); in case similar of NONE => the (mk_star' pures' (mk_star' true_t rt)) | SOME (t1,t2) => let val t_stripped = remove_term t1 (remove_term t2 t); in mk_star t_stripped (mk_star t1 t2) end end; fun skip_ex ((exq as Const (@{const_name "ex_assn"},_))$(Abs (n,ty,t))) = exq$Abs (n,ty,skip_ex t) | skip_ex t = normalize_core t; val (bs,t') = strip_abs t; val ty = fastype_of1 (map #2 bs,t'); in if ty = @{typ assn} then Logic.rlist_abs (bs,skip_ex t') else t end; (*val _ = tracing (tr_term redex);*) val (f,terms) = strip_comb redex; val nterms = map (fn t => let (*val _ = tracing (tr_term t); *) val t'=normalize t; (*val _ = tracing (tr_term t');*) in t' end) terms; val new_form = list_comb (f,nterms); val res_ss = (put_simpset HOL_basic_ss ctxt addsimps @{thms star_aci}); val result = Option.map (export o mk_meta_eq) (Arith_Data.prove_conv_nohyps [simp_tac res_ss 1] ctxt' (redex,new_form) ); in result - end handle exc => - if Exn.is_interrupt exc then Exn.reraise exc - else - (tracing ("assn_simproc failed with exception\n:" ^ Runtime.exn_message exc); - NONE) (* Fail silently *); + end catch exc => + (tracing ("assn_simproc failed with exception\n:" ^ Runtime.exn_message exc); + NONE) (* Fail silently *) + \ val assn_simproc = Simplifier.make_simproc @{context} "assn_simproc" {lhss = [@{term "h \ P"}, @{term "P \\<^sub>A Q"}, @{term "P \\<^sub>t Q"}, @{term "Hoare_Triple.hoare_triple P c Q"}, @{term "(P::assn) = Q"}], proc = K assn_simproc_fun}; (***********************************) (* Default Simplifications *) (***********************************) (* Default simplification. MUST contain assertion normalization! Tactic must not fail! *) fun dflt_tac ctxt = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimprocs [assn_simproc] addsimps @{thms norm_assertion_simps} addsimps (Named_Theorems.get ctxt @{named_theorems sep_dflt_simps}) |> fold Splitter.del_split @{thms if_split} ); (***********************************) (* Frame Matcher *) (***********************************) (* Do frame matching imp_solve_tac - tactic used to discharge first assumption of match-rule cf. lemma FI_match. *) fun match_frame_tac imp_solve_tac ctxt = let (* Normalize star-lists *) val norm_tac = simp_tac ( put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_normalize}); (* Strip star-lists *) val strip_tac = simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_strip}) THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_def}); (* Do a match step *) val match_tac = resolve_tac ctxt @{thms FI_match} (* Separate p,q*) THEN' SOLVED' imp_solve_tac (* Solve implication *) THEN' norm_tac; (* Do a no-match step *) val nomatch_tac = resolve_tac ctxt @{thms FI_p_nomatch} ORELSE' (resolve_tac ctxt @{thms FI_q_nomatch} THEN' norm_tac); in resolve_tac ctxt @{thms FI_init} THEN' norm_tac THEN' REPEAT_DETERM' (FIRST' [ CHANGED o dflt_tac ctxt, (match_tac ORELSE' nomatch_tac)]) THEN' resolve_tac ctxt @{thms FI_finalize} THEN' strip_tac end; (***********************************) (* Frame Inference *) (***********************************) fun frame_inference_tac ctxt = resolve_tac ctxt @{thms frame_inference_init} THEN' match_frame_tac (resolve_tac ctxt @{thms ent_refl}) ctxt THEN' resolve_tac ctxt @{thms frame_inference_finalize}; (***********************************) (* Entailment Solver *) (***********************************) (* Extract existential quantifiers from entailment goal *) fun extract_ex_tac ctxt i st = let fun count_ex (Const (@{const_name Assertions.entails},_)$_$c) = count_ex c RS @{thm HOL.mp} | count_ex (Const (@{const_name Assertions.ex_assn},_)$Abs (_,_,t)) = count_ex t RS @{thm enorm_exI'} | count_ex _ = @{thm imp_refl}; val concl = Logic.concl_of_goal (Thm.prop_of st) i |> HOLogic.dest_Trueprop; val thm = count_ex concl; in (TRY o REPEAT_ALL_NEW (match_tac ctxt @{thms ent_ex_preI}) THEN' resolve_tac ctxt [thm]) i st end; (* Solve Entailment *) fun solve_entails_tac ctxt = let val preprocess_entails_tac = dflt_tac ctxt THEN' extract_ex_tac ctxt THEN' simp_tac (put_simpset HOL_ss ctxt addsimps @{thms solve_ent_preprocess_simps}); val match_entails_tac = resolve_tac ctxt @{thms entails_solve_init} THEN' match_frame_tac (resolve_tac ctxt @{thms ent_refl}) ctxt THEN' resolve_tac ctxt @{thms entails_solve_finalize}; in preprocess_entails_tac THEN' (TRY o REPEAT_ALL_NEW (match_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems sep_eintros})))) THEN_ALL_NEW (dflt_tac ctxt THEN' TRY o (match_tac ctxt @{thms ent_triv} ORELSE' resolve_tac ctxt @{thms ent_refl} ORELSE' match_entails_tac)) end; (***********************************) (* Verification Condition Generator*) (***********************************) fun heap_rule_tac ctxt h_thms = resolve_tac ctxt h_thms ORELSE' ( resolve_tac ctxt @{thms fi_rule} THEN' (resolve_tac ctxt h_thms THEN_IGNORE_NEWGOALS frame_inference_tac ctxt)); fun vcg_step_tac ctxt = let val h_thms = rev (Named_Theorems.get ctxt @{named_theorems sep_heap_rules}); val d_thms = rev (Named_Theorems.get ctxt @{named_theorems sep_decon_rules}); val heap_rule_tac = heap_rule_tac ctxt h_thms (* Apply consequence rule if postcondition is not a schematic var *) fun app_post_cons_tac i st = case Logic.concl_of_goal (Thm.prop_of st) i |> HOLogic.dest_Trueprop of Const (@{const_name Hoare_Triple.hoare_triple},_)$_$_$qt => if is_Var (head_of qt) then no_tac st else resolve_tac ctxt @{thms cons_post_rule} i st | _ => no_tac st; in CSUBGOAL (snd #> (FIRST' [ CHANGED o dflt_tac ctxt, REPEAT_ALL_NEW (resolve_tac ctxt @{thms normalize_rules}), CHANGED o (FIRST' [resolve_tac ctxt d_thms, heap_rule_tac] ORELSE' (app_post_cons_tac THEN' FIRST' [resolve_tac ctxt d_thms, heap_rule_tac])) ])) end; fun vcg_tac ctxt = REPEAT_DETERM' (vcg_step_tac ctxt) (***********************************) (* Automatic Solver *) (***********************************) fun sep_autosolve_tac do_pre do_post ctxt = let val pre_tacs = [ CHANGED o clarsimp_tac ctxt, CHANGED o REPEAT_ALL_NEW (match_tac ctxt @{thms ballI allI impI conjI}) ]; val main_tacs = [ match_tac ctxt @{thms is_hoare_triple} THEN' CHANGED o vcg_tac ctxt, match_tac ctxt @{thms is_entails} THEN' CHANGED o solve_entails_tac ctxt ]; val post_tacs = [SELECT_GOAL (auto_tac ctxt)]; val tacs = (if do_pre then pre_tacs else []) @ main_tacs @ (if do_post then post_tacs else []); in REPEAT_DETERM' (CHANGED o FIRST' tacs) end; (***********************************) (* Method Setup *) (***********************************) val dflt_simps_modifiers = [ Args.$$$ "dflt_simps" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_dflt_simps}) \<^here>), Args.$$$ "dflt_simps" -- Scan.option Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_dflt_simps}) \<^here>) ]; val heap_modifiers = [ Args.$$$ "heap" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_heap_rules}) \<^here>), Args.$$$ "heap" -- Scan.option Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_heap_rules}) \<^here>) ]; val decon_modifiers = [ Args.$$$ "decon" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_decon_rules}) \<^here>), Args.$$$ "decon" -- Scan.option Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_decon_rules}) \<^here>) ]; val eintros_modifiers = [ Args.$$$ "eintros" -- Scan.option Args.add -- Args.colon >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_eintros}) \<^here>), Args.$$$ "eintros" -- Scan.option Args.del -- Args.colon >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_eintros}) \<^here>) ]; val solve_entails_modifiers = dflt_simps_modifiers @ eintros_modifiers; val vcg_modifiers = heap_modifiers @ decon_modifiers @ dflt_simps_modifiers; val sep_auto_modifiers = clasimp_modifiers @ vcg_modifiers @ eintros_modifiers; end; \ simproc_setup assn_simproc ("h\P" | "P\\<^sub>AQ" | "P\\<^sub>tQ" | "

c " | "(P::assn) = Q") = \K Seplogic_Auto.assn_simproc_fun\ method_setup assn_simp =\Scan.succeed (fn ctxt => (SIMPLE_METHOD' ( CHANGED o Seplogic_Auto.dflt_tac ctxt )))\ "Seplogic: Simplification of assertions" method_setup frame_inference = \Scan.succeed (fn ctxt => (SIMPLE_METHOD' ( CHANGED o Seplogic_Auto.frame_inference_tac ctxt )))\ "Seplogic: Frame inference" method_setup solve_entails = \ Method.sections Seplogic_Auto.solve_entails_modifiers >> (fn _ => fn ctxt => SIMPLE_METHOD' ( CHANGED o Seplogic_Auto.solve_entails_tac ctxt ))\ "Seplogic: Entailment Solver" method_setup heap_rule = \ Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' ( let val thms = case thms of [] => rev (Named_Theorems.get ctxt @{named_theorems sep_heap_rules}) | _ => thms in CHANGED o Seplogic_Auto.heap_rule_tac ctxt thms end ))\ "Seplogic: Apply rule with frame inference" method_setup vcg = \ Scan.lift (Args.mode "ss") -- Method.sections Seplogic_Auto.vcg_modifiers >> (fn (ss,_) => fn ctxt => SIMPLE_METHOD' ( CHANGED o ( if ss then Seplogic_Auto.vcg_step_tac ctxt else Seplogic_Auto.vcg_tac ctxt ) ))\ "Seplogic: Verification Condition Generator" method_setup sep_auto = \Scan.lift (Args.mode "nopre" -- Args.mode "nopost" -- Args.mode "plain") --| Method.sections Seplogic_Auto.sep_auto_modifiers >> (fn ((nopre,nopost),plain) => fn ctxt => SIMPLE_METHOD' ( CHANGED o Seplogic_Auto.sep_autosolve_tac ((not nopre) andalso (not plain)) ((not nopost) andalso (not plain)) ctxt ))\ "Seplogic: Automatic solver" lemmas [sep_dflt_simps] = split declare deconstruct_rules[sep_decon_rules] declare heap_rules[sep_heap_rules] lemmas [sep_eintros] = impI conjI exI subsection \Semi-Automatic Reasoning\ text \In this section, we provide some lemmas for semi-automatic reasoning\ text \Forward reasoning with frame. Use \frame_inference\-method to discharge second assumption.\ lemma ent_frame_fwd: assumes R: "P \\<^sub>A R" assumes F: "Ps \\<^sub>A P*F" assumes I: "R*F \\<^sub>A Q" shows "Ps \\<^sub>A Q" using assms by (metis ent_refl ent_star_mono ent_trans) lemma mod_frame_fwd: assumes M: "h\Ps" assumes R: "P\\<^sub>AR" assumes F: "Ps \\<^sub>A P*F" shows "h\R*F" using assms by (metis ent_star_mono entails_def) text \Apply precision rule with frame inference.\ lemma prec_frame: assumes PREC: "precise P" assumes M1: "h\(R1 \\<^sub>A R2)" assumes F1: "R1 \\<^sub>A P x p * F1" assumes F2: "R2 \\<^sub>A P y p * F2" shows "x=y" using preciseD[OF PREC] M1 F1 F2 by (metis entailsD mod_and_dist) lemma prec_frame_expl: assumes PREC: "\x y. (h\(P x * F1) \\<^sub>A (P y * F2)) \ x=y" assumes M1: "h\(R1 \\<^sub>A R2)" assumes F1: "R1 \\<^sub>A P x * F1" assumes F2: "R2 \\<^sub>A P y * F2" shows "x=y" using assms by (metis entailsD mod_and_dist) text \Variant that is useful within induction proofs, where induction goes over \x\ or \y\\ lemma prec_frame': assumes PREC: "(h\(P x * F1) \\<^sub>A (P y * F2)) \ x=y" assumes M1: "h\(R1 \\<^sub>A R2)" assumes F1: "R1 \\<^sub>A P x * F1" assumes F2: "R2 \\<^sub>A P y * F2" shows "x=y" using assms by (metis entailsD mod_and_dist) lemma ent_wand_frameI: assumes "(Q -* R) * F \\<^sub>A S" assumes "P \\<^sub>A F * X" assumes "Q*X \\<^sub>A R" shows "P \\<^sub>A S" using assms by (metis ent_frame_fwd ent_wandI mult.commute) subsubsection \Manual Frame Inference\ lemma ent_true_drop: "P\\<^sub>AQ*true \ P*R\\<^sub>AQ*true" "P\\<^sub>AQ \ P\\<^sub>AQ*true" apply (metis assn_times_comm ent_star_mono ent_true merge_true_star_ctx) apply (metis assn_one_left ent_star_mono ent_true star_aci(2)) done lemma fr_refl: "A\\<^sub>AB \ A*C \\<^sub>AB*C" by (blast intro: ent_star_mono ent_refl) lemma fr_rot: "(A*B \\<^sub>A C) \ (B*A \\<^sub>A C)" by (simp add: assn_aci) lemma fr_rot_rhs: "(A \\<^sub>A B*C) \ (A \\<^sub>A C*B)" by (simp add: assn_aci) lemma ent_star_mono_true: assumes "A \\<^sub>A A' * true" assumes "B \\<^sub>A B' * true" shows "A*B*true \\<^sub>A A'*B'*true" using ent_star_mono[OF assms] apply simp using ent_true_drop(1) by blast lemma ent_refl_true: "A \\<^sub>A A * true" by (simp add: ent_true_drop(2)) lemma entt_fr_refl: "F\\<^sub>tF' \ F*A \\<^sub>t F'*A" by (rule entt_star_mono) auto lemma entt_fr_drop: "F\\<^sub>tF' \ F*A \\<^sub>t F'" using ent_true_drop(1) enttD enttI by blast method_setup fr_rot = \ let fun rot_tac ctxt = resolve_tac ctxt @{thms fr_rot} THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms star_assoc[symmetric]}) in Scan.lift Parse.nat >> (fn n => fn ctxt => SIMPLE_METHOD' ( fn i => REPEAT_DETERM_N n (rot_tac ctxt i))) end \ method_setup fr_rot_rhs = \ let fun rot_tac ctxt = resolve_tac ctxt @{thms fr_rot_rhs} THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms star_assoc[symmetric]}) in Scan.lift Parse.nat >> (fn n => fn ctxt => SIMPLE_METHOD' ( fn i => REPEAT_DETERM_N n (rot_tac ctxt i))) end \ (*<*) subsection \Test Cases\ lemma "\x. A x * true * Q x \\<^sub>A true * A x * Q x" apply simp done lemma "A * (true * B) \\<^sub>A true * A * B" apply (simp) done lemma "h\true*P*true \ h\P*true" by simp lemma "A * true * \(b \ c) * true * B \\<^sub>A \b * \c * true *A * B" by simp lemma "\y c. \\<^sub>Ax. P x * (R x * Q y) * \ (b \ c) \\<^sub>A (\\<^sub>Ax. \b * (P x * (R x * Q y) * \c))" apply simp done lemma "A * B * (\c * B * C * D * \a * true * \d) * (\\<^sub>Ax. E x * F * \b) * true \\<^sub>A (\\<^sub>Ax. \ (c \ a \ d \ b) * true * A * B * (true * B * C * D) * (E x * F))" apply simp done lemma "

c <\r. Q r * true * \(b r) * true * \a> \

c <\r. Q r * true * \(b r \ a)>" apply simp done lemma "(h\((A*B*\b*true*\c*true) \\<^sub>A (\(p=q)*P*Q))) \ h \ A * B * true \\<^sub>A P * Q \ b \ c \ p = q" apply simp done lemma assumes "FI_RESULT [(B, B), (A, A)] C D F" shows "FI_QUERY (A*B*C) (D*B*A) F" apply (tactic \Seplogic_Auto.match_frame_tac (resolve_tac @{context} @{thms ent_refl}) @{context} 1\) by (rule assms) lemma assumes "FI_RESULT [(B,B), (A,A)] C emp F" shows "FI_QUERY (A*B*C) (B*A) F" apply (tactic \Seplogic_Auto.match_frame_tac (resolve_tac @{context} @{thms ent_refl}) @{context} 1\) by (rule assms) lemma assumes "FI_RESULT [(B, B), (A, A)] emp emp F" shows "FI_QUERY (A*B) (B*A) F" apply (tactic \Seplogic_Auto.match_frame_tac (resolve_tac @{context} @{thms ent_refl}) @{context} 1\) by (rule assms) lemma assumes "FI_RESULT [(A, A)] emp emp F" shows "FI_QUERY (A) (A) F" apply (tactic \Seplogic_Auto.match_frame_tac (resolve_tac @{context} @{thms ent_refl}) @{context} 1\) by (rule assms) lemma assumes "FI_RESULT [(A, A)] (B * C * D) emp F" shows "FI_QUERY (B*C*D*A) (A) F" apply (tactic \Seplogic_Auto.match_frame_tac (resolve_tac @{context} @{thms ent_refl}) @{context} 1\) by (rule assms) schematic_goal "P1 * P2 * P3 * P4 \\<^sub>A P3 * ?R1" "P1 * (P2 * (P3 * P4)) \\<^sub>A P1 * ?R2" "P4 * (P2 * (P1 * P3)) \\<^sub>A P1 * ?R2'" "P1 * P2 * P3 * P4 \\<^sub>A P4 * ?R3" "P1 * P2 \\<^sub>A P1 * ?R4" "P1 * P2 \\<^sub>A P2 * ?R5" "P1 \\<^sub>A P1 * ?R6" "P1 * P2 \\<^sub>A emp * ?R7" by frame_inference+ lemma "\A; B; C; b 17\ \ Q 1 5 3 \\<^sub>A (\\<^sub>Ax y z. \\<^sub>Aa. Q x y z * \(b a) * \(y=5))" by solve_entails thm nth_rule lemma "

\<^sub>a[1,2,3]> do { v\Array_Time.nth x 1; return v } <\r. P * x\\<^sub>a[1,2,3] * \(r=2)>" apply sep_auto done (*>*) subsection \Quick Overview of Proof Methods\ text_raw \\label{sec:auto:overview}\ text \ In this section, we give a quick overview of the available proof methods and options. The most versatile proof method that we provide is \sep_auto\. It tries to solve the first subgoal, invoking appropriate proof methods as required. If it cannot solve the subgoal completely, it stops at the intermediate state that it could not handle any more. \sep_auto\ can be configured by section-arguments for the simplifier, the classical reasoner, and all section-arguments for the verification condition generator and entailment solver. Moreover, it takes an optional mode argument (mode), where valid modes are: \begin{description} \item[(nopre)] No preprocessing of goal. The preprocessor tries to clarify and simplify the goal before the main method is invoked. \item[(nopost)] No postprocessing of goal. The postprocessor tries to solve or simplify goals left over by verification condition generation or entailment solving. \item[(plain)] Neither pre- nor postprocessing. Just applies vcg and entailment solver. \end{description} \paragraph{Entailment Solver.} The entailment solver processes goals of the form \P \\<^sub>A Q\. It is invoked by the method \solve_entails\. It first tries to pull out pure parts of \P\ and \Q\. This may introduce quantifiers, conjunction, and implication into the goal, that are eliminated by resolving with rules declared as \sep_eintros\ (method argument: eintros[add/del]:). Moreover, it simplifies with rules declared as \sep_dflt_simps\ (section argument: \dflt_simps[add/del]:\). Now, \P\ and \Q\ should have the form \X\<^sub>1*\*X\<^sub>n\. Then, the frame-matcher is used to match all items of \P\ with items of \Q\, and thus solve the implication. Matching is currently done syntactically, but can instantiate schematic variables. Note that, by default, existential introduction is declared as \sep_eintros\-rule. This introduces schematic variables, that can later be matched against. However, in some cases, the matching may instantiate the schematic variables in an undesired way. In this case, the argument \eintros del: exI\ should be passed to the entailment solver, and the existential quantifier should be instantiated manually. \paragraph{Frame Inference} The method \frame_inference\ tries to solve a goal of the form \P\Q*?F\, by matching \Q\ against the parts of \P\, and instantiating \?F\ accordingly. Matching is done syntactically, possibly instantiating schematic variables. \P\ and \Q\ should be assertions separated by \*\. Note that frame inference does no simplification or other kinds of normalization. The method \heap_rule\ applies the specified heap rules, using frame inference if necessary. If no rules are specified, the default heap rules are used. \paragraph{Verification Condition Generator} The verification condition generator processes goals of the form \

c\. It is invoked by the method \vcg\. First, it tries to pull out pure parts and simplifies with the default simplification rules. Then, it tries to resolve the goal with deconstruct rules (attribute: \sep_decon_rules\, section argument: \decon[add/del]:\), and if this does not succeed, it tries to resolve the goal with heap rules (attribute: \sep_heap_rules\, section argument: \heap[add/del]:\), using the frame rule and frame inference. If resolving is not possible, it also tries to apply the consequence rule to make the postcondition a schematic variable. \ (*<*) subsection \Hiding of internal stuff\ hide_const (open) FI SLN (*>*) end