# HG changeset patch # User wenzelm # Date 1434987883 -7200 # Node ID 742b553d88b2b159d1f2e1df3958430af29acb9d # Parent 2b8342b0d98cbb5c1d059be46b25778d73f86cba tuned whitespace; diff -r 2b8342b0d98c -r 742b553d88b2 src/HOL/Eisbach/eisbach_rule_insts.ML --- a/src/HOL/Eisbach/eisbach_rule_insts.ML Mon Jun 22 16:48:27 2015 +0200 +++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Mon Jun 22 17:44:43 2015 +0200 @@ -87,7 +87,7 @@ map snd type_insts |> Syntax.read_typs ctxt1; - val typ_insts' = map2 (fn (xi, _) => fn T => (xi,T)) type_insts typs; + val typ_insts' = map2 (fn (xi, _) => fn T => (xi, T)) type_insts typs; val terms = map snd term_insts @@ -95,7 +95,7 @@ val term_insts' = map2 (fn (xi, _) => fn t => (xi, t)) term_insts terms; - in (typ_insts',term_insts') end; + in (typ_insts', term_insts') end; datatype rule_inst = @@ -153,7 +153,7 @@ val _ = (insts', term_insts) |> ListPair.app (fn (SOME p, SOME t) => Parse_Tools.the_parse_fun p t | _ => ()); - val (insts'',concl_insts'') = chop (length insts) term_insts; + val (insts'', concl_insts'') = chop (length insts) term_insts; in Unchecked_Term_Insts (insts'', concl_insts'') end; fun read_of_insts checked context ((insts, concl_insts), fixes) = diff -r 2b8342b0d98c -r 742b553d88b2 src/HOL/Eisbach/match_method.ML --- a/src/HOL/Eisbach/match_method.ML Mon Jun 22 16:48:27 2015 +0200 +++ b/src/HOL/Eisbach/match_method.ML Mon Jun 22 17:44:43 2015 +0200 @@ -342,33 +342,28 @@ val outer_env = morphism_env morphism env; val thm' = Morphism.thm morphism thm; in inst_thm ctxt outer_env params ts thm' end - | export_with_params _ morphism (NONE,_) thm _ = Morphism.thm morphism thm; + | export_with_params _ morphism (NONE, _) thm _ = Morphism.thm morphism thm; fun match_filter_env is_newly_fixed pat_vars fixes params env = let val param_vars = map Term.dest_Var params; val tenv = Envir.term_env env; - val params' = map (fn (xi, _) => Vartab.lookup tenv xi) param_vars; val fixes_vars = map Term.dest_Var fixes; val all_vars = Vartab.keys tenv; - val extra_vars = subtract (fn ((xi, _), xi') => xi = xi') fixes_vars all_vars; val tenv' = tenv |> fold (Vartab.delete_safe) extra_vars; - val env' = Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv', tyenv = Envir.type_env env} - val all_params_bound = forall (fn SOME (_, Free (x,_)) => is_newly_fixed x | _ => false) params'; - + val all_params_bound = forall (fn SOME (_, Free (x, _)) => is_newly_fixed x | _ => false) params'; val all_params_distinct = not (has_duplicates (op =) params'); val pat_fixes = inter (eq_fst (op =)) fixes_vars pat_vars; - val all_pat_fixes_bound = forall (fn (xi, _) => is_some (Vartab.lookup tenv' xi)) pat_fixes; in if all_params_bound andalso all_pat_fixes_bound andalso all_params_distinct @@ -413,7 +408,7 @@ val ct = Drule.mk_term (hyp) |> Thm.cprop_of; in Drule.protect (Conjunction.mk_conjunction (ident, ct)) end; -fun hyp_from_ctermid ctxt (ident,cterm) = +fun hyp_from_ctermid ctxt (ident, cterm) = let val ident = Thm.cterm_of ctxt (HOLogic.mk_number @{typ nat} ident |> Logic.mk_term); in Drule.protect (Conjunction.mk_conjunction (ident, cterm)) end; @@ -468,13 +463,13 @@ fun prem_from_hyp hyp goal = let val asm = Thm.assume hyp; - val (identt,ct) = asm |> Goal.conclude |> Thm.cprop_of |> Conjunction.dest_conjunction; + val (identt, ct) = asm |> Goal.conclude |> Thm.cprop_of |> Conjunction.dest_conjunction; val ident = HOLogic.dest_number (Thm.term_of identt |> Logic.dest_term) |> snd; val thm = Conjunction.intr (solve_term identt) (solve_term ct) |> Goal.protect 0 val goal' = Thm.implies_elim (Thm.implies_intr hyp goal) thm; in - (SOME (ident,ct),goal') - end handle TERM _ => (NONE,goal) | THM _ => (NONE,goal); + (SOME (ident, ct), goal') + end handle TERM _ => (NONE, goal) | THM _ => (NONE, goal); in fold_map prem_from_hyp chyps goal |>> map_filter I @@ -486,7 +481,7 @@ let val {context, params, prems, asms, concl, schematics} = focus; - val (prem_ids,ctxt') = context + val (prem_ids, ctxt') = context |> add_focus_params params |> add_focus_schematics (snd schematics) |> fold_map add_focus_prem (rev prems) @@ -495,12 +490,13 @@ val ctxt'' = fold add_premid_hyp local_prems ctxt'; in - (prem_ids,{context = ctxt'', - params = params, - prems = prems, - concl = concl, - schematics = schematics, - asms = asms}) + (prem_ids, + {context = ctxt'', + params = params, + prems = prems, + concl = concl, + schematics = schematics, + asms = asms}) end; @@ -541,32 +537,32 @@ forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv) end; -fun term_eq_wrt (env1,env2) (t1,t2) = +fun term_eq_wrt (env1, env2) (t1, t2) = Envir.eta_contract (Envir.norm_term env1 t1) aconv Envir.eta_contract (Envir.norm_term env2 t2); -fun type_eq_wrt (env1,env2) (T1,T2) = - Envir.norm_type (Envir.type_env env1) T1 = Envir.norm_type (Envir.type_env env2) T2 +fun type_eq_wrt (env1, env2) (T1, T2) = + Envir.norm_type (Envir.type_env env1) T1 = Envir.norm_type (Envir.type_env env2) T2; fun eq_env (env1, env2) = Envir.maxidx_of env1 = Envir.maxidx_of env1 andalso ListPair.allEq (fn ((var, (_, t)), (var', (_, t'))) => - (var = var' andalso term_eq_wrt (env1,env2) (t,t'))) + (var = var' andalso term_eq_wrt (env1, env2) (t, t'))) (apply2 Vartab.dest (Envir.term_env env1, Envir.term_env env2)) andalso ListPair.allEq (fn ((var, (_, T)), (var', (_, T'))) => - var = var' andalso type_eq_wrt (env1,env2) (T,T')) + var = var' andalso type_eq_wrt (env1, env2) (T, T')) (apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2)); -fun merge_env (env1,env2) = +fun merge_env (env1, env2) = let val tenv = Vartab.merge (eq_snd (term_eq_wrt (env1, env2))) (Envir.term_env env1, Envir.term_env env2); val tyenv = Vartab.merge (eq_snd (type_eq_wrt (env1, env2)) andf eq_fst (op =)) - (Envir.type_env env1,Envir.type_env env2); + (Envir.type_env env1, Envir.type_env env2); val maxidx = Int.max (Envir.maxidx_of env1, Envir.maxidx_of env2); in Envir.Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv} end; @@ -600,7 +596,7 @@ fun do_cut n = if n = ~1 then I else Seq.take n; val raw_thmss = map (get o snd) prop_pats; - val (thmss,ctxt') = fold_burrow import_with_tags raw_thmss ctxt; + val (thmss, ctxt') = fold_burrow import_with_tags raw_thmss ctxt; val newly_fixed = Variable.is_newly_fixed ctxt' ctxt; @@ -619,7 +615,7 @@ |> Seq.filter consistent_env |> Seq.map_filter (fn env' => (case match_filter_env newly_fixed pat_vars fixes params env' of - SOME env'' => SOME (export_with_params ctxt morphism (ts,params) thm env',env'') + SOME env'' => SOME (export_with_params ctxt morphism (ts, params) thm env', env'') | NONE => NONE)) |> Seq.map (apfst (Thm.map_tags (K (Thm.get_tags thm)))) |> deduplicate (eq_pair Thm.eq_thm_prop eq_env) [] @@ -642,7 +638,7 @@ Seq_retrieve envthms (fn (env, _) => eq_env (env, env')); in (case result of - SOME (_,thms) => SOME ((env', thm :: thms), maximal_set tail seq' envthms') + SOME (_, thms) => SOME ((env', thm :: thms), maximal_set tail seq' envthms') | NONE => Seq.pull (maximal_set (tail @ [(env', [thm])]) seq' envthms')) end | NONE => Seq.pull (Seq.append envthms (Seq.of_list tail)))); @@ -660,8 +656,8 @@ else let fun just_one (thm, env') = - (case try_merge (env,env') of - SOME env'' => SOME ((pat,[thm]) :: pats, env'') + (case try_merge (env, env') of + SOME env'' => SOME ((pat, [thm]) :: pats, env'') | NONE => NONE); in fold (fn seq => Seq.append (Seq.map_filter just_one seq)) thmenvs Seq.empty end); @@ -713,9 +709,9 @@ | Match_Concl => g | _ => raise Fail "Match kind fell through"); - val (goal_thins,goal) = get_thinned_prems goal; + val (goal_thins, goal) = get_thinned_prems goal; - val ((local_premids,{context = focus_ctxt, params, asms, concl, ...}), focused_goal) = + val ((local_premids, {context = focus_ctxt, params, asms, concl, ...}), focused_goal) = focus_cases (K Subgoal.focus_prems) (focus_concl) ctxt 1 goal |>> augment_focus; @@ -725,7 +721,7 @@ make_fact_matches focus_ctxt (Item_Net.retrieve (focus_prems focus_ctxt |> snd) #> filter_out (member (eq_fst (op =)) goal_thins) - #> is_local ? filter (fn (p,_) => exists (fn id' => id' = p) local_premids) + #> is_local ? filter (fn (p, _) => exists (fn id' => id' = p) local_premids) #> order_list)) (fn _ => make_term_matches focus_ctxt (fn _ => [Logic.strip_imp_concl (Thm.term_of concl)])) @@ -735,7 +731,7 @@ fun do_retrofit inner_ctxt goal' = let - val (goal'_thins,goal') = get_thinned_prems goal'; + val (goal'_thins, goal') = get_thinned_prems goal'; val thinned_prems = ((subtract (eq_fst (op =)) @@ -750,7 +746,7 @@ thinned_prems @ map (fn (id, prem) => (id, (NONE, SOME prem))) (goal'_thins @ goal_thins); - val (thinned_local_prems,thinned_extra_prems) = + val (thinned_local_prems, thinned_extra_prems) = List.partition (fn (id, _) => member (op =) local_premids id) all_thinned_prems; val local_thins = diff -r 2b8342b0d98c -r 742b553d88b2 src/HOL/Eisbach/method_closure.ML --- a/src/HOL/Eisbach/method_closure.ML Mon Jun 22 16:48:27 2015 +0200 +++ b/src/HOL/Eisbach/method_closure.ML Mon Jun 22 17:44:43 2015 +0200 @@ -91,7 +91,7 @@ if exists is_free_thm (thm :: args) then dummy_free_thm else f context thm); -fun free_aware_attribute thy {handle_all_errs,declaration} src (context, thm) = +fun free_aware_attribute thy {handle_all_errs, declaration} src (context, thm) = let val src' = Token.init_assignable_src src; fun apply_att thm = (Attrib.attribute_global thy src') (context, thm); @@ -270,16 +270,16 @@ fun dummy_named_thm named_thm ctxt = let val ctxt' = empty_named_thm named_thm ctxt; - val (_,ctxt'') = Thm.proof_attributes [Named_Theorems.add named_thm] dummy_free_thm ctxt'; + val (_, ctxt'') = Thm.proof_attributes [Named_Theorems.add named_thm] dummy_free_thm ctxt'; in ctxt'' end; fun parse_method_args method_names = let - fun bind_method (name, text) ctxt = - let - val method = method_evaluate text; - val inner_update = method o update_dynamic_method (name,K (method ctxt)); - in update_dynamic_method (name,inner_update) ctxt end; + fun bind_method (name, text) ctxt = + let + val method = method_evaluate text; + val inner_update = method o update_dynamic_method (name, K (method ctxt)); + in update_dynamic_method (name, inner_update) ctxt end; fun do_parse t = parse_method >> pair t; fun rep [] x = Scan.succeed [] x @@ -349,7 +349,7 @@ (parse_term_args args -- parse_method_args method_names --| (Scan.depend (fn context => - Scan.succeed (Context.map_proof (fold empty_named_thm uses_nms) context,())) -- + Scan.succeed (Context.map_proof (fold empty_named_thm uses_nms) context, ())) -- Method.sections modifiers) >> eval); val lthy3 = lthy2