diff --git a/thys/Akra_Bazzi/akra_bazzi.ML b/thys/Akra_Bazzi/akra_bazzi.ML --- a/thys/Akra_Bazzi/akra_bazzi.ML +++ b/thys/Akra_Bazzi/akra_bazzi.ML @@ -1,630 +1,630 @@ (* Title: akra_bazzi.ML Author: Manuel Eberl, TU Muenchen *) signature AKRA_BAZZI = sig val master_theorem_tac : string option -> bool -> thm option -> term option -> term option -> term option -> Proof.context -> int -> tactic val master_theorem_function_tac : bool -> Proof.context -> int -> tactic val akra_bazzi_term_tac : Proof.context -> int -> tactic val akra_bazzi_sum_tac : Proof.context -> int -> tactic val akra_bazzi_relation_tac : Proof.context -> int -> tactic val akra_bazzi_measure_tac : Proof.context -> int -> tactic val akra_bazzi_termination_tac : Proof.context -> int -> tactic val setup_master_theorem : Context.generic * Token.T list -> (Proof.context -> Method.method) * (Context.generic * Token.T list) end structure Akra_Bazzi: AKRA_BAZZI = struct fun changed_conv conv ct = let val thm = conv ct in if Thm.is_reflexive thm then raise CTERM ("changed_conv", [ct]) else thm end fun rewrite_tac ctxt thms = CONVERSION (Conv.repeat_conv (changed_conv (Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv (map (fn thm => thm RS @{thm eq_reflection}) thms)))) ctxt))) val term_preps = @{thms akra_bazzi_termination_simps} fun get_term_intros ctxt = Named_Theorems.get ctxt @{named_theorems "akra_bazzi_term_intros"} val master_intros = @{thms master_theorem_function.master1_automation master_theorem_function.master1_bigo_automation master_theorem_function.master1_automation' master_theorem_function.master1_bigo_automation' master_theorem_function.master2_1_automation master_theorem_function.master2_1_automation' master_theorem_function.master2_2_automation master_theorem_function.master2_2_automation' master_theorem_function.master2_3_automation master_theorem_function.master2_3_automation' master_theorem_function.master3_automation master_theorem_function.master3_automation'} fun get_intros NONE b = if not b then master_intros else @{thms master_theorem_function.master1_automation master_theorem_function.master1_bigo_automation master_theorem_function.master1_automation' master_theorem_function.master2_1_automation master_theorem_function.master2_1_automation'} | get_intros (SOME "1") _ = @{thms master_theorem_function.master1_automation master_theorem_function.master1_bigo_automation master_theorem_function.master1_automation' master_theorem_function.master1_bigo_automation'} | get_intros (SOME "2.1") _ = @{thms master_theorem_function.master2_1_automation master_theorem_function.master2_1_automation'} | get_intros (SOME "2.2") _ = @{thms master_theorem_function.master2_2_automation master_theorem_function.master2_2_automation'} | get_intros (SOME "2.3") _ = @{thms master_theorem_function.master2_3_automation master_theorem_function.master2_3_automation'} | get_intros (SOME "3") _ = @{thms master_theorem_function.master3_automation master_theorem_function.master3_automation'} | get_intros _ _ = error "invalid Master theorem case" val allowed_consts = [@{term "(+) :: nat => nat => nat"}, @{term "Suc :: nat => nat"}, @{term "(+) :: real => real => real"}, @{term "(-) :: real => real => real"}, @{term "uminus :: real => real"}, @{term "(*) :: real => real => real"}, @{term "(/) :: real => real => real"}, @{term "inverse :: real => real"}, @{term "(powr) :: real => real => real"}, @{term "real_of_nat"}, @{term "real :: nat => real"}, @{term "Num.numeral :: num => real"}, @{term "Num.Bit0"}, @{term "Num.Bit1"}, @{term "0 :: real"}, @{term "1 :: real"}, @{term "Num.One"}, @{term "Num.BitM"}, @{term "Num.numeral :: num => nat"}, @{term "0 :: nat"}, @{term "1 :: nat"}, @{term "atLeastAtMost :: real => real => real set"}, @{term "greaterThanAtMost :: real => real => real set"}, @{term "atLeastLessThan :: real => real => real set"}, @{term "greaterThanLessThan :: real => real => real set"}, @{term "(=) :: real => real => bool"}, @{term "(\) :: real => real => bool"}, @{term "(<) :: real => real => bool"}, @{term "(\) :: real => real set => bool"}, @{term "(=) :: nat => nat => bool"}, @{term "(\) :: nat => nat => bool"}, @{term "(<) :: nat => nat => bool"}, @{term "Trueprop"}, @{term "HOL.Not"}, @{term "HOL.conj"}, @{term "HOL.disj"}, @{term "HOL.implies"}] fun contains_only_numerals t = let fun go (s $ t) = let val _ = go s in go t end | go (Const c) = if member (op =) allowed_consts (Const c) then () else raise TERM ("contains_only_numerals", [Const c]) | go t = raise TERM ("contains_only_numerals", [t]) val _ = go t in true end handle TERM _ => false fun dest_nat_number t = case HOLogic.dest_number t of (ty, n) => if ty = @{typ "Nat.nat"} then n else raise TERM ("dest_nat_number", [t]) fun num_to_Suc n = let fun go acc 0 = acc | go acc n = go (@{term "Suc :: Nat.nat => Nat.nat"} $ acc) (n - 1) in go @{term "0 :: Nat.nat"} n end (* Termination *) datatype breadcrumb = Fst | Snd (* extract all natural number types from a product type *) fun pick_natT_leaf T = let fun go crumbs T acc = case try HOLogic.dest_prodT T of SOME (T1, T2) => acc |> go (Snd :: crumbs) T2 |> go (Fst :: crumbs) T1 | NONE => if T = HOLogic.natT then crumbs :: acc else acc in go [] T [] end fun breadcrumb Fst = fst | breadcrumb Snd = snd (* construct an extractor function using fst/snd from a path in a product type *) fun mk_extractor T crumbs = let fun aux c f (T', acc) = let val T'' = HOLogic.dest_prodT T' |> f in (T'', Const (c, T' --> T'') $ acc) end fun go [] (_, acc) = Abs ("n", T, acc) | go (Fst :: crumbs) acc = acc |> aux @{const_name fst} fst |> go crumbs | go (Snd :: crumbs) acc = acc |> aux @{const_name snd} snd |> go crumbs in go (rev crumbs) (T, Bound 0) end fun extract_from_prod [] t = t | extract_from_prod (c :: cs) t = extract_from_prod cs t |> HOLogic.dest_prod |> breadcrumb c fun ANY' tacs n = fold (curry op APPEND) (map (fn t => t n) tacs) no_tac (* find recursion variable, set up a measure function for it and apply it to prove termination *) fun akra_bazzi_relation_tac ctxt = case Proof_Context.lookup_fact ctxt "local.termination" of SOME {thms = [thm], ...} => let val prems = Thm.prems_of thm val relT = prems |> hd |> dest_comb |> snd |> dest_comb |> snd |> dest_Var |> snd val T = relT |> HOLogic.dest_setT |> HOLogic.dest_prodT |> fst val prems = prems |> tl |> map Term.strip_all_body val calls = prems |> map (Logic.strip_imp_concl #> HOLogic.dest_Trueprop #> dest_comb #> fst #> dest_comb #> snd #> HOLogic.dest_prod #> fst) val leaves = pick_natT_leaf T val calls = map (fn path => (path, map (extract_from_prod path) calls)) leaves val calls = calls |> filter (snd #> filter is_Bound #> null) |> map fst val measureC = Const (@{const_name Wellfounded.measure}, (T --> HOLogic.natT) --> relT) fun mk_relation f = measureC $ f val relations = map (mk_relation o mk_extractor T) calls in (ANY' (map (Function_Relation.relation_tac ctxt o K) relations) THEN' resolve_tac ctxt @{thms wf_measure}) THEN_ALL_NEW (rewrite_tac ctxt @{thms measure_prod_conv measure_prod_conv'}) end | _ => K no_tac val measure_postproc_simps = @{thms arith_simps of_nat_0 of_nat_1 of_nat_numeral Suc_numeral of_nat_Suc} (* prove that the measure decreases in a recursive call by showing that the recursive call is an Akra-Bazzi term. Apply simple post-processing to make the numbers less ugly *) fun akra_bazzi_measure_tac ctxt = rewrite_tac ctxt term_preps THEN' eresolve_tac ctxt @{thms akra_bazzi_term_measure} THEN' resolve_tac ctxt (get_term_intros ctxt) THEN_ALL_NEW rewrite_tac ctxt measure_postproc_simps (* prove termination of an Akra-Bazzi function *) fun akra_bazzi_termination_tac ctxt = akra_bazzi_relation_tac ctxt THEN_ALL_NEW akra_bazzi_measure_tac ctxt (* General preprocessing *) fun nat_numeral_conv ctxt ct = let val t = Thm.term_of ct val prop = Logic.mk_equals (t, num_to_Suc (dest_nat_number t)) fun tac goal_ctxt = SOLVE (Local_Defs.unfold_tac goal_ctxt @{thms eval_nat_numeral BitM.simps One_nat_def} THEN resolve_tac goal_ctxt @{thms Pure.reflexive} 1); in case \<^try>\Goal.prove ctxt [] [] prop (tac o #context)\ of NONE => raise CTERM ("nat_numeral_conv", [ct]) | SOME thm => thm end fun akra_bazzi_sum_conv ctxt ct = case Thm.term_of ct of (Const (@{const_name sum}, _) $ _ $ (Const (@{const_name Set_Interval.ord_class.lessThan}, _) $ _)) => Conv.arg_conv (Conv.arg_conv (nat_numeral_conv ctxt)) ct | _ => raise CTERM ("akra_bazzi_sum_conv", [ct]) fun akra_bazzi_sum_tac ctxt i = let fun conv ctxt = Conv.try_conv (akra_bazzi_sum_conv ctxt) val thms = @{thms eval_akra_bazzi_sum eval_akra_bazzi_sum' mult_1_left mult_1_right add_0_left add_0_right} in CHANGED (CONVERSION (Conv.top_conv conv ctxt) i THEN REPEAT (EqSubst.eqsubst_tac ctxt [0] thms i)) end fun akra_bazzi_term_tac ctxt = rewrite_tac ctxt term_preps THEN' (resolve_tac ctxt (get_term_intros ctxt)) fun akra_bazzi_terms_tac ctxt = REPEAT_ALL_NEW (fn i => DETERM (resolve_tac ctxt @{thms akra_bazzi_termsI'} i)) THEN_ALL_NEW akra_bazzi_term_tac ctxt fun analyze_terminal ctxt f x inv t_orig t acc = let val thy = Proof_Context.theory_of ctxt val patvar = ("x",1) val pat = Term.betapply (f, Var (patvar, HOLogic.natT)) fun match t = let val matcher = Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty) val x' = Vartab.lookup (snd matcher) patvar |> the |> snd in if Term.exists_subterm (fn x' => x = x') x' then x' else raise Pattern.MATCH end fun add_term t (acc, acc_inv, call) = if inv then (acc, t :: acc_inv, call) else (t :: acc, acc_inv, call) fun go t (acc, acc_inv, call) = let val call' = match t in case call of NONE => (acc, acc_inv, SOME call') | SOME _ => raise TERM ("Non-linear occurrence of recursive call", [t_orig]) end handle Pattern.MATCH => add_term t (acc, acc_inv, call) in go t acc end; fun mk_prod [] = @{term "1 :: real"} | mk_prod (x::xs) = fold (fn x => fn acc => @{term "(*) :: real => real => real"} $ x $ acc) xs x fun mk_quot (xs, []) = mk_prod xs | mk_quot ([], ys) = @{term "inverse :: real => real"} $ mk_prod ys | mk_quot (xs, ys) = @{term "(/) :: real => real => real"} $ mk_prod xs $ mk_prod ys fun analyze_prod ctxt f x minus t (acc1, acc2) = let fun go inv (oper $ t1 $ t2) acc = if oper = @{term "(*) :: real => real => real"} then go inv t1 (go inv t2 acc) else if oper = @{term "(/) :: real => real => real"} then go inv t1 (go (not inv) t2 acc) else analyze_terminal ctxt f x inv t (oper $ t1 $ t2) acc | go inv (oper $ t') acc = if oper = @{term "inverse :: real => real"} then go (not inv) t' acc else analyze_terminal ctxt f x inv t (oper $ t') acc | go inv t' acc = analyze_terminal ctxt f x inv t t' acc in case go false t ([], [], NONE) of (_, _, NONE) => (acc1, (if minus then @{term "uminus :: real => real"} $ t else t) :: acc2) | (xs, ys, SOME call) => let val r = mk_quot (xs, ys) val r' = (if minus then @{term "uminus :: real => real"} $ r else r, call) in (r' :: acc1, acc2) end end fun mk_sum [] = @{term "0 :: real"} | mk_sum (x::xs) = let fun go (f $ x) acc = if f = @{term "uminus :: real => real"} then @{term "(-) :: real => real => real"} $ acc $ x else @{term "(+) :: real => real => real"} $ acc $ (f $ x) | go x acc = @{term "(+) :: real => real => real"} $ acc $ x in fold go xs x end fun analyze_sum ctxt f x t = let fun go minus (oper $ t1 $ t2) acc = if oper = @{term "(+) :: real => real => real"} then go minus t1 (go minus t2 acc) else if oper = @{term "(-) :: real => real => real"} then go minus t1 (go (not minus) t2 acc) else analyze_prod ctxt f x minus (oper $ t1 $ t2) acc | go minus (oper $ t) acc = if oper = @{term "uminus :: real => real"} then go (not minus) t acc else analyze_prod ctxt f x minus (oper $ t) acc | go minus t acc = analyze_prod ctxt f x minus t acc in case go false t ([],[]) of (xs,ys) => (xs, mk_sum ys) end fun extract_coeff ctxt t = let val thy = Proof_Context.theory_of ctxt val t' = Raw_Simplifier.rewrite_term thy @{thms akra_bazzi_termination_simps[THEN eq_reflection]} [] t fun aux thm = let val (tmp, pat) = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> Term.dest_comb val var = tmp |> Term.dest_comb |> snd |> Term.dest_Var |> fst val (_, insts) = Pattern.first_order_match thy (pat, t') (Vartab.empty, Vartab.empty) val coeff = Option.map snd (Vartab.lookup insts var) in coeff end handle Pattern.MATCH => NONE in case get_first aux (get_term_intros ctxt) of NONE => raise TERM ("extract_coeff", [t']) | SOME coeff => coeff end fun get_var_name (Free (x, _)) = x | get_var_name (Var ((x,_),_)) = x | get_var_name t = raise TERM ("get_var_name", [t]) fun analyze_call ctxt f x t = let val (ts, g) = analyze_sum ctxt f x t val k = length ts val a_coeffs = HOLogic.mk_list HOLogic.realT (map fst ts) fun abstract t = Abs (get_var_name x, HOLogic.natT, abstract_over (x, t)) val ts = map (abstract o snd) ts val b_coeffs = HOLogic.mk_list HOLogic.realT (map (extract_coeff ctxt) ts) val ts = HOLogic.mk_list (HOLogic.natT --> HOLogic.natT) ts in {k = HOLogic.mk_nat k, a_coeffs = a_coeffs, b_coeffs = b_coeffs, ts = ts, g = abstract g} end fun instantiate_akra_bazzi ctxt ts = map (Thm.instantiate' [] (map (Option.map (Thm.cterm_of ctxt)) ts)) fun analyze_equation ctxt f eq funvar = let val rhs = eq |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd val {k, a_coeffs, b_coeffs, ts, g} = analyze_call ctxt f funvar rhs in {k = k, a_coeffs = a_coeffs, b_coeffs = b_coeffs, ts = ts, f = f, g = g} end fun akra_bazzi_instantiate_tac ctxt f eq x0 x1 funvar p' = let val {k, a_coeffs, b_coeffs, ts, g, ...} = analyze_equation ctxt f eq funvar val insts = ([SOME x0, SOME x1, SOME k, SOME a_coeffs, SOME b_coeffs, SOME ts, SOME f, SOME g] @ (filter Option.isSome [p'])) in resolve_tac ctxt o instantiate_akra_bazzi ctxt insts end (* val code_simp_tac = Code_Simp.static_tac {consts = [@{const_name arith_consts}], ctxt = @{context}, simpset = NONE} fun eval_real_numeral_conv ctxt ct = case Thm.term_of ct of @{term "Pure.imp"} $ _ $ _ => Conv.implies_concl_conv (eval_real_numeral_conv ctxt) ct | _ => let val t = Thm.term_of ct val prop = Logic.mk_equals (t, @{term "Trueprop True"}) fun tac goal_ctxt = let val ctxt' = put_simpset (simpset_of @{context}) goal_ctxt in Local_Defs.unfold_tac ctxt' @{thms greaterThanLessThan_iff} THEN (SOLVE (Simplifier.full_simp_tac ctxt' 1) ORELSE code_simp_tac ctxt' 1) end in if contains_only_numerals t then case \<^try>\Goal.prove ctxt [] [] prop (tac o #context)\ of SOME thm => thm | NONE => raise CTERM ("eval_real_numeral_conv", [ct]) else raise CTERM ("eval_real_numeral_conv", [ct]) end *) fun eval_numeral_tac ctxt = SUBGOAL (fn (goal, i) => if contains_only_numerals (Logic.strip_imp_concl goal) then Eval_Numeral.eval_numeral_tac ctxt i else all_tac) fun unfold_simps ctxt = rewrite_tac ctxt @{thms eval_akra_bazzi_le_list_ex eval_length of_nat_numeral of_nat_0 of_nat_1 numeral_One} (* Applying the locale intro rule *) fun master_theorem_function_tac simp ctxt = resolve_tac ctxt @{thms master_theorem_functionI} THEN_ALL_NEW ((fn i => TRY (REPEAT_ALL_NEW (match_tac ctxt @{thms ball_set_intros}) i)) THEN_ALL_NEW ((fn i => TRY (akra_bazzi_terms_tac ctxt i)) THEN_ALL_NEW (fn i => unfold_simps ctxt i THEN TRY (akra_bazzi_sum_tac ctxt i) THEN unfold_simps ctxt i THEN (if simp then TRY (eval_numeral_tac ctxt i) else all_tac) ) ) ) (* Pre-processing of Landau bound in goal and post-processing of Landau bounds in premises *) fun goal_conv conv ct = case Thm.term_of ct of (Const (@{const_name "Pure.imp"}, _) $ _ $ _) => Conv.arg_conv (goal_conv conv) ct | _ => conv ct fun rewrs_conv' thms = goal_conv (Conv.arg_conv (Conv.arg_conv (Conv.rewrs_conv thms))) fun preprocess_tac ctxt = CONVERSION (rewrs_conv' @{thms CLAMP}) THEN' rewrite_tac ctxt @{thms propagate_CLAMP CLAMP_aux} THEN' rewrite_tac ctxt @{thms CLAMP_postproc} THEN' CONVERSION (rewrs_conv' @{thms UNCLAMP'}) fun rewrs_goal_conv thms = goal_conv (Conv.arg_conv (Conv.arg_conv (Conv.rewrs_conv thms))) fun rewrs_conv thms ctxt = Conv.repeat_conv (changed_conv (Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv thms))) ctxt)) fun postprocess_tac ctxt = TRY o ( CONVERSION (rewrs_goal_conv @{thms CLAMP}) THEN' rewrite_tac ctxt @{thms CLAMP_aux} THEN' rewrite_tac ctxt @{thms CLAMP_postproc} THEN' CONVERSION (rewrs_conv @{thms MASTER_BOUND_postproc[THEN eq_reflection]} ctxt) THEN' CONVERSION (rewrs_conv @{thms MASTER_BOUND_UNCLAMP[THEN eq_reflection]} ctxt) THEN' CONVERSION (rewrs_goal_conv @{thms UNCLAMP})) (* The main tactic *) fun intros_tac ctxt thms = DETERM o TRY o REPEAT_ALL_NEW (DETERM o match_tac ctxt thms) fun master_theorem_tac' caseno simp f eq funvar x0 x1 p' ctxt = ( preprocess_tac ctxt THEN' akra_bazzi_instantiate_tac ctxt f eq x0 x1 funvar p' (get_intros caseno (p' <> NONE)) THEN' DETERM o master_theorem_function_tac simp ctxt) THEN_ALL_NEW intros_tac ctxt @{thms ball_set_intros akra_bazzi_p_rel_intros} THEN_ALL_NEW (DETERM o ( unfold_simps ctxt THEN' TRY o akra_bazzi_sum_tac ctxt THEN' unfold_simps ctxt THEN' postprocess_tac ctxt THEN' (if simp then TRY o eval_numeral_tac ctxt else K all_tac) THEN' intros_tac ctxt @{thms allI ballI conjI impI} THEN_ALL_NEW (TRY o eresolve_tac ctxt @{thms atLeastLessThanE}))) fun find_function goal = case goal |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop of @{term "Set.member :: (nat => real) => _ set => bool"} $ f $ _ => f | _ => raise TERM ("find_function", [goal]) val leq_nat = @{term "(<=) :: nat => nat => bool"} val less_nat = @{term "(<) :: nat => nat => bool"} fun find_x1 var eq = let fun get_x1 prem = case prem |> HOLogic.dest_Trueprop of rel $ x1 $ x => if x = var andalso rel = leq_nat then SOME x1 else if x = var andalso rel = less_nat then SOME (@{term "Suc"} $ x1) else NONE | _ => NONE in get_first get_x1 (Thm.prems_of eq) end handle TERM _ => NONE fun analyze_funeq pat var ctxt eq = let val lhs = eq |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst val matcher = Thm.first_order_match (Thm.cterm_of ctxt lhs, pat) val eq = Thm.instantiate matcher eq in case find_x1 var eq of NONE => NONE | SOME _ => SOME eq end handle Pattern.MATCH => NONE fun find_funeq ctxt f = let val n = ("n", 0) val n' = Var (n, HOLogic.natT) val pat = Thm.cterm_of ctxt (Term.betapply (f, n')) fun get_function_info (Abs (_, _, body)) = get_function_info body | get_function_info (t as f $ _) = (Function.get_info ctxt t handle Empty => get_function_info f) | get_function_info t = Function.get_info ctxt t val {simps = simps, ...} = get_function_info f handle List.Empty => raise TERM ("Could not obtain function info record.", [f]) val simps = case simps of SOME simps => simps | NONE => raise TERM ("Function has no simp rules.", [f]) in case get_first (analyze_funeq pat n' ctxt) simps of SOME s => (s, n') | NONE => raise TERM ("Could not determine recurrence from simp rules.", [f]) end fun master_theorem_tac caseno simp eq x0 x1 p' ctxt = SUBGOAL (fn (goal, i) => Subgoal.FOCUS (fn {context = ctxt, ...} => let val f = find_function goal val (eq, funvar) = case eq of SOME eq => ( let val n = Var (("n", 0), HOLogic.natT) in case (analyze_funeq (Thm.cterm_of ctxt (f $ n)) n ctxt eq) of SOME eq => (eq, n) | NONE => raise TERM ("", []) end handle TERM _ => raise TERM ( "Could not determine recursion variable from recurrence theorem.", [Thm.prop_of eq])) | NONE => find_funeq ctxt f val x0 = Option.getOpt (x0, @{term "0::nat"}) val x1 = if Option.isSome x1 then x1 else find_x1 funvar eq val x1 = case x1 of SOME x1 => x1 | NONE => raise TERM ("Could not determine x1 from recurrence theorem", [goal, Thm.prop_of eq, funvar]) val p' = if caseno = NONE orelse caseno = SOME "1" orelse caseno = SOME "2.1" then p' else NONE in HEADGOAL (master_theorem_tac' caseno simp f eq funvar x0 x1 p' ctxt) end ) ctxt i) handle TERM _ => K no_tac fun read_term_with_type ctxt T = Syntax.check_term ctxt o Type.constraint T o Syntax.parse_term ctxt fun parse_assoc key scan = Scan.lift (Args.$$$ key -- Args.colon) -- scan >> snd val parse_param = let fun term_with_type T = - Scan.peek (fn context => Args.embedded_inner_syntax >> + Scan.peek (fn context => Parse.embedded_inner_syntax >> read_term_with_type (Context.proof_of context) T); in parse_assoc "recursion" Attrib.thm >> (fn x => (SOME x, NONE, NONE, NONE)) || parse_assoc "x0" (term_with_type HOLogic.natT) >> (fn x => (NONE, SOME x, NONE, NONE)) || parse_assoc "x1" (term_with_type HOLogic.natT) >> (fn x => (NONE, NONE, SOME x, NONE)) || parse_assoc "p'" (term_with_type HOLogic.realT) >> (fn x => (NONE, NONE, NONE, SOME x)) end val parse_params = let fun add_option NONE y = y | add_option x _ = x fun go (a,b,c,d) (a',b',c',d') = (add_option a a', add_option b b', add_option c c', add_option d d') in Scan.repeat parse_param >> (fn xs => fold go xs (NONE, NONE, NONE, NONE)) end val setup_master_theorem = Scan.option (Scan.lift (Parse.number || Parse.float_number)) -- Scan.lift (Args.parens (Args.$$$ "nosimp") >> K false || Scan.succeed true) -- parse_params >> (fn ((caseno, simp), (thm, x0, x1, p')) => fn ctxt => let val _ = case caseno of SOME caseno => if member (op =) ["1","2.1","2.2","2.3","3"] caseno then () else cat_error "illegal Master theorem case: " caseno | NONE => () in SIMPLE_METHOD' (master_theorem_tac caseno simp thm x0 x1 p' ctxt) end) end; diff --git a/thys/Auto2_HOL/util.ML b/thys/Auto2_HOL/util.ML --- a/thys/Auto2_HOL/util.ML +++ b/thys/Auto2_HOL/util.ML @@ -1,925 +1,925 @@ (* File: util.ML Author: Bohua Zhan Utility functions. *) signature BASIC_UTIL = sig (* Exceptions *) val assert: bool -> string -> unit (* Types *) val propT: typ (* Lists *) val the_pair: 'a list -> 'a * 'a val the_triple: 'a list -> 'a * 'a * 'a val filter_split: ('a -> bool) -> 'a list -> 'a list * 'a list (* Managing matching environments. *) val fo_init: Type.tyenv * Envir.tenv val lookup_instn: Type.tyenv * Envir.tenv -> string * int -> term val lookup_inst: Type.tyenv * Envir.tenv -> string -> term (* Tracing functions. *) val trace_t: Proof.context -> string -> term -> unit val trace_tlist: Proof.context -> string -> term list -> unit val trace_thm: Proof.context -> string -> thm -> unit val trace_fullthm: Proof.context -> string -> thm -> unit val trace_thm_global: string -> thm -> unit val trace_fullthm_global: string -> thm -> unit (* Terms *) val dest_arg: term -> term val dest_arg1: term -> term (* Theorems *) val apply_to_thm: conv -> thm -> thm val meta_sym: thm -> thm val apply_to_lhs: conv -> thm -> thm val apply_to_rhs: conv -> thm -> thm end; signature UTIL = sig include BASIC_UTIL (* Lists *) val max: ('a * 'a -> order) -> 'a list -> 'a val max_partial: ('a -> 'a -> bool) -> 'a list -> 'a list val subsets: 'a list -> 'a list list val all_permutes: 'a list -> 'a list list val all_pairs: 'a list * 'b list -> ('a * 'b) list val remove_dup_lists: ('a * 'a -> order) -> 'a list * 'a list -> 'a list * 'a list val is_subseq: ('a * 'a -> bool) -> 'a list * 'a list -> bool (* Strings. *) val is_prefix_str: string -> string -> bool val is_just_internal: string -> bool (* Managing matching environments. *) val defined_instn: Type.tyenv * Envir.tenv -> string * int -> bool val lookup_tyinst: Type.tyenv * Envir.tenv -> string -> typ val update_env: indexname * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv val eq_env: (Type.tyenv * Envir.tenv) * (Type.tyenv * Envir.tenv) -> bool (* Matching. *) val first_order_match_list: theory -> (term * term) list -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv (* Printing functions, mostly from Isabelle Cookbook. *) val string_of_terms: Proof.context -> term list -> string val string_of_terms_global: theory -> term list -> string val string_of_tyenv: Proof.context -> Type.tyenv -> string val string_of_env: Proof.context -> Envir.tenv -> string val string_of_list: ('a -> string) -> 'a list -> string val string_of_list': ('a -> string) -> 'a list -> string val string_of_bool: bool -> string (* Managing context. *) val declare_free_term: term -> Proof.context -> Proof.context (* Terms. *) val is_abs: term -> bool val is_implies: term -> bool val dest_binop: term -> term * (term * term) val dest_binop_head: term -> term val dest_binop_args: term -> term * term val dest_args: term -> term list val dest_argn: int -> term -> term val get_head_name: term -> string val is_meta_eq: term -> bool val occurs_frees: term list -> term -> bool val occurs_free: term -> term -> bool val has_vars: term -> bool val is_subterm: term -> term -> bool val has_subterm: term list -> term -> bool val is_head: term -> term -> bool val lambda_abstract: term -> term -> term val is_pattern_list: term list -> bool val is_pattern: term -> bool val normalize_meta_all_imp: Proof.context -> conv val swap_meta_imp_alls: Proof.context -> conv val normalize_meta_horn: Proof.context -> conv val strip_meta_horn: term -> term list * (term list * term) val list_meta_horn: term list * (term list * term) -> term val to_internal_vars: Proof.context -> term list * term -> term list * term val rename_abs_term: term list -> term -> term val print_term_detail: Proof.context -> term -> string (* cterms. *) val dest_cargs: cterm -> cterm list val dest_binop_cargs: cterm -> cterm * cterm (* Theorems. *) val arg_backn_conv: int -> conv -> conv val argn_conv: int -> conv -> conv val comb_equiv: cterm * thm list -> thm val name_of_thm: thm -> string val update_name_of_thm: thm -> string -> thm -> thm val lhs_of: thm -> term val rhs_of: thm -> term val assume_meta_eq: theory -> term * term -> thm val assume_thm: Proof.context -> term -> thm val subst_thm_thy: theory -> Type.tyenv * Envir.tenv -> thm -> thm val subst_thm: Proof.context -> Type.tyenv * Envir.tenv -> thm -> thm val send_first_to_hyps: thm -> thm val send_all_to_hyps: thm -> thm val subst_thm_atomic: (cterm * cterm) list -> thm -> thm val subst_term_norm: Type.tyenv * Envir.tenv -> term -> term val concl_conv_n: int -> conv -> conv val concl_conv: conv -> conv val transitive_list: thm list -> thm val skip_n_conv: int -> conv -> conv val pattern_rewr_conv: term -> (term * thm) list -> conv val eq_cong_th: int -> term -> term -> Proof.context -> thm val forall_elim_sch: thm -> thm (* Conversions *) val reverse_eta_conv: Proof.context -> conv val repeat_n_conv: int -> conv -> conv (* Miscellaneous. *) val test_conv: Proof.context -> conv -> string -> string * string -> unit val term_pat_setup: theory -> theory val cterm_pat_setup: theory -> theory val type_pat_setup: theory -> theory val timer: string * (unit -> 'a) -> 'a val exn_trace: (unit -> 'a) -> 'a end; structure Util : UTIL = struct fun assert b exn_str = if b then () else raise Fail exn_str val propT = @{typ prop} fun max comp lst = let fun max2 t1 t2 = if comp (t1, t2) = LESS then t2 else t1 in case lst of [] => raise Fail "max: empty list" | l :: ls => fold max2 ls l end (* Given a function comp, remove y for each pair (x, y) such that comp x y = true (if x dominates y). *) fun max_partial comp lst = let fun helper taken remains = case remains of [] => taken | x :: xs => if exists (fn y => comp y x) taken then helper taken xs else helper (x :: filter_out (fn y => comp x y) taken) xs in helper [] lst end (* Return all subsets of lst. *) fun subsets [] = [[]] | subsets (l::ls) = let val prev = subsets ls in prev @ map (cons l) prev end (* List of all permutations of xs *) fun all_permutes xs = case xs of [] => [[]] | [x] => [[x]] | [x, y] => [[x, y], [y, x]] | _ => maps (fn i => map (cons (nth xs i)) (all_permutes (nth_drop i xs))) (0 upto (length xs - 1)) (* Convert list to pair. List must consist of exactly two items. *) fun the_pair lst = case lst of [i1, i2] => (i1, i2) | _ => raise Fail "the_pair" (* Convert list to triple. List must consist of exactly three items. *) fun the_triple lst = case lst of [i1, i2, i3] => (i1, i2, i3) | _ => raise Fail "the_triple" (* Split list into (ins, outs), where ins satisfy f, and outs don't. *) fun filter_split _ [] = ([], []) | filter_split f (x :: xs) = let val (ins, outs) = filter_split f xs in if f x then (x :: ins, outs) else (ins, x :: outs) end (* Form the Cartesian product of two lists. *) fun all_pairs (l1, l2) = maps (fn y => (map (fn x => (x, y)) l1)) l2 (* Given two sorted lists, remove all pairs of terms that appear in both lists, counting multiplicity. *) fun remove_dup_lists ord (xs, ys) = case xs of [] => ([], ys) | x :: xs' => case ys of [] => (xs, []) | y :: ys' => case ord (x, y) of LESS => apfst (cons x) (remove_dup_lists ord (xs', ys)) | EQUAL => remove_dup_lists ord (xs', ys') | GREATER => apsnd (cons y) (remove_dup_lists ord (xs, ys')) (* Whether l1 is a subsequence of l2. *) fun is_subseq eq (l1, l2) = case l1 of [] => true | x :: l1' => case l2 of [] => false | y :: l2' => if eq (x, y) then is_subseq eq (l1', l2') else is_subseq eq (l1, l2') (* Whether pre is a prefix of str. *) fun is_prefix_str pre str = is_prefix (op =) (String.explode pre) (String.explode str) (* Test whether x is followed by exactly one _. *) fun is_just_internal x = Name.is_internal x andalso not (Name.is_skolem x) val fo_init = (Vartab.empty, Vartab.empty) (* Lookup a Vartab inst with string and integer specifying indexname. *) fun defined_instn (_, inst) (str, n) = Vartab.defined inst (str, n) fun lookup_instn (_, inst) (str, n) = case Vartab.lookup inst (str, n) of NONE => raise Fail ("lookup_inst: not found " ^ str ^ (if n = 0 then "" else string_of_int n)) | SOME (_, u) => u fun lookup_inst (tyinst, inst) str = lookup_instn (tyinst, inst) (str, 0) fun lookup_tyinst (tyinst, _) str = case Vartab.lookup tyinst (str, 0) of NONE => raise Fail ("lookup_tyinst: not found " ^ str) | SOME (_, T) => T fun update_env (idx, t) (tyenv, tenv) = (tyenv, tenv |> Vartab.update_new (idx, (type_of t, t))) (* A rough comparison, simply compare the corresponding terms. *) fun eq_env ((_, inst1), (_, inst2)) = let val data1 = Vartab.dest inst1 val data2 = Vartab.dest inst2 fun compare_data (((x, i), (ty, t)), ((x', i'), (ty', t'))) = x = x' andalso i = i' andalso ty = ty' andalso t aconv t' in eq_set compare_data (data1, data2) end fun first_order_match_list thy pairs inst = case pairs of [] => inst | (t, u) :: rest => let val inst' = Pattern.first_order_match thy (t, u) inst in first_order_match_list thy rest inst' end fun string_of_terms ctxt ts = ts |> map (Syntax.pretty_term ctxt) |> Pretty.commas |> Pretty.block |> Pretty.string_of fun string_of_terms_global thy ts = ts |> map (Syntax.pretty_term_global thy) |> Pretty.commas |> Pretty.block |> Pretty.string_of fun pretty_helper aux env = env |> Vartab.dest |> map aux |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2]) |> Pretty.enum "," "[" "]" |> Pretty.string_of fun string_of_tyenv ctxt tyenv = let fun get_typs (v, (s, T)) = (TVar (v, s), T) val print = apply2 (Syntax.pretty_typ ctxt) in pretty_helper (print o get_typs) tyenv end fun string_of_env ctxt env = let fun get_ts (v, (T, t)) = (Var (v, T), t) val print = apply2 (Syntax.pretty_term ctxt) in pretty_helper (print o get_ts) env end fun string_of_list func lst = Pretty.str_list "[" "]" (map func lst) |> Pretty.string_of fun string_of_list' func lst = if length lst = 1 then func (the_single lst) else string_of_list func lst fun string_of_bool b = if b then "true" else "false" fun trace_t ctxt s t = tracing (s ^ " " ^ (Syntax.string_of_term ctxt t)) fun trace_tlist ctxt s ts = tracing (s ^ " " ^ (string_of_terms ctxt ts)) fun trace_thm ctxt s th = tracing (s ^ " " ^ (th |> Thm.prop_of |> Syntax.string_of_term ctxt)) fun trace_fullthm ctxt s th = tracing (s ^ " [" ^ (Thm.hyps_of th |> string_of_terms ctxt) ^ "] ==> " ^ (Thm.prop_of th |> Syntax.string_of_term ctxt)) fun trace_thm_global s th = let val thy = Thm.theory_of_thm th in tracing (s ^ " " ^ (th |> Thm.prop_of |> Syntax.string_of_term_global thy)) end fun trace_fullthm_global s th = let val thy = Thm.theory_of_thm th in tracing (s ^ " [" ^ (Thm.hyps_of th |> string_of_terms_global thy) ^ "] ==> " ^ (Thm.prop_of th |> Syntax.string_of_term_global thy)) end fun declare_free_term t ctxt = if not (is_Free t) then raise Fail "declare_free_term: t not free." else ctxt |> Variable.add_fixes_direct [t |> Term.dest_Free |> fst] |> Variable.declare_term t fun is_abs t = case t of Abs _ => true | _ => false (* Whether a given term is of the form A ==> B. *) fun is_implies t = let val _ = assert (fastype_of t = propT) "is_implies: wrong type" in case t of @{const Pure.imp} $ _ $ _ => true | _ => false end (* Extract the last two arguments on t, collecting the rest into f. *) fun dest_binop t = case t of f $ a $ b => (f, (a, b)) | _ => raise Fail "dest_binop" fun dest_binop_head t = fst (dest_binop t) fun dest_binop_args t = snd (dest_binop t) (* Return the argument of t. If t is f applied to multiple arguments, return the last argument. *) fun dest_arg t = case t of _ $ arg => arg | _ => raise Fail "dest_arg" (* Return the first of two arguments of t. *) fun dest_arg1 t = case t of _ $ arg1 $ _ => arg1 | _ => raise Fail "dest_arg1" (* Return the list of all arguments of t. *) fun dest_args t = t |> Term.strip_comb |> snd (* Return the nth argument of t, counting from left and starting at zero. *) fun dest_argn n t = nth (dest_args t) n (* Return the name of the head function. *) fun get_head_name t = case Term.head_of t of Const (nm, _) => nm | _ => raise Fail "get_head_name" (* Whether the term is of the form A == B. *) fun is_meta_eq t = let val _ = assert (fastype_of t = propT) "is_meta_eq_term: wrong type" in case t of Const (@{const_name Pure.eq}, _) $ _ $ _ => true | _ => false end (* Given free variable freevar (or a list of free variables freevars), determine whether any of the inputs appears in t. *) fun occurs_frees freevars t = inter (op aconv) (map Free (Term.add_frees t [])) freevars <> [] fun occurs_free freevar t = occurs_frees [freevar] t (* Whether the given term contains schematic variables. *) fun has_vars t = length (Term.add_vars t []) > 0 (* Whether subt is a subterm of t. *) fun is_subterm subt t = exists_subterm (fn t' => t' aconv subt) t (* Whether any of subts is a subterm of t. *) fun has_subterm subts t = exists_subterm (fn t' => member (op aconv) subts t') t (* Whether s is a head term of t. *) fun is_head s t = let val (sf, sargs) = Term.strip_comb s val (tf, targs) = Term.strip_comb t in sf aconv tf andalso is_prefix (op aconv) sargs targs end (* If stmt is P(t), return %t. P(t). *) fun lambda_abstract t stmt = Term.lambda t (Term.abstract_over (t, stmt)) (* A more general criterion for patterns. In combinations, any argument that is a pattern (in the more general sense) frees up checking for any functional schematic variables in that argument. *) fun is_pattern_list ts = let fun is_funT T = case T of Type ("fun", _) => true | _ => false fun get_fun_vars t = (Term.add_vars t []) |> filter (is_funT o snd) |> map Var fun test_list exclude_vars ts = case ts of [] => true | [t] => test_term exclude_vars t | t :: ts' => if test_term exclude_vars t then test_list (merge (op aconv) (exclude_vars, get_fun_vars t)) ts' else if test_list exclude_vars ts' then test_term (distinct (op aconv) (exclude_vars @ maps get_fun_vars ts')) t else false and test_term exclude_vars t = case t of Abs (_, _, t') => test_term exclude_vars t' | _ => let val (head, args) = strip_comb t in if is_Var head then if member (op aconv) exclude_vars head then test_list exclude_vars args else forall is_Bound args andalso not (has_duplicates (op aconv) args) else test_list exclude_vars args end in test_list [] ts end fun is_pattern t = is_pattern_list [t] (* Push !!x to the right as much as possible. *) fun normalize_meta_all_imp_once ct = Conv.try_conv ( Conv.every_conv [Conv.rewr_conv (Thm.symmetric @{thm Pure.norm_hhf_eq}), Conv.arg_conv normalize_meta_all_imp_once]) ct fun normalize_meta_all_imp ctxt ct = let val t = Thm.term_of ct in if Logic.is_all t then Conv.every_conv [Conv.binder_conv (normalize_meta_all_imp o snd) ctxt, normalize_meta_all_imp_once] ct else if is_implies t then Conv.arg_conv (normalize_meta_all_imp ctxt) ct else Conv.all_conv ct end (* Rewrite A ==> !!v_i. B to !!v_i. A ==> B. *) fun swap_meta_imp_alls ctxt ct = let val t = Thm.term_of ct in if is_implies t andalso Logic.is_all (dest_arg t) then Conv.every_conv [Conv.rewr_conv @{thm Pure.norm_hhf_eq}, Conv.binder_conv (swap_meta_imp_alls o snd) ctxt] ct else Conv.all_conv ct end (* Normalize a horn clause into standard form !!v_i. A_i ==> B. *) fun normalize_meta_horn ctxt ct = let val t = Thm.term_of ct in if Logic.is_all t then Conv.binder_conv (normalize_meta_horn o snd) ctxt ct else if is_implies t then Conv.every_conv [Conv.arg_conv (normalize_meta_horn ctxt), swap_meta_imp_alls ctxt] ct else Conv.all_conv ct end (* Deconstruct a horn clause !!v_i. A_i ==> B into (v_i, (A_i, B)). *) fun strip_meta_horn t = case t of Const (@{const_name Pure.all}, _) $ (u as Abs _) => let val (v, body) = Term.dest_abs_global u val (vars, (assums, concl)) = strip_meta_horn body in (Free v :: vars, (assums, concl)) end | @{const Pure.imp} $ P $ Q => let val (vars, (assums, concl)) = strip_meta_horn Q in (vars, (P :: assums, concl)) end | _ => ([], ([], t)) fun list_meta_horn (vars, (As, B)) = (Logic.list_implies (As, B)) |> fold Logic.all (rev vars) fun to_internal_vars ctxt (vars, body) = let val vars' = vars |> map Term.dest_Free |> Variable.variant_frees ctxt [] |> map (apfst Name.internal) |> map Free val subst = vars ~~ vars' in (vars', subst_atomic subst body) end fun rename_abs_term vars t = case vars of [] => t | var :: rest => let val (x, _) = Term.dest_Free var in case t of A $ Abs (_, T1, body) => A $ Abs (x, T1, rename_abs_term rest body) | _ => error "rename_abs_term" end fun print_term_detail ctxt t = case t of Const (s, ty) => "Const (" ^ s ^ ", " ^ (Syntax.string_of_typ ctxt ty) | Free (s, ty) => "Free (" ^ s ^ ", " ^ (Syntax.string_of_typ ctxt ty) ^ ")" | Var ((x, i), ty) => "Var ((" ^ x ^ ", " ^ (string_of_int i) ^ "), " ^ (Syntax.string_of_typ ctxt ty) ^ ")" | Bound n => "Bound " ^ (string_of_int n) | Abs (s, ty, b) => "Abs (" ^ s ^ ", " ^ (Syntax.string_of_typ ctxt ty) ^ ", " ^ (print_term_detail ctxt b) ^ ")" | u $ v => "(" ^ print_term_detail ctxt u ^ ") $ (" ^ print_term_detail ctxt v ^ ")" (* Version for ct. *) fun dest_cargs ct = ct |> Drule.strip_comb |> snd fun dest_binop_cargs ct = (Thm.dest_arg1 ct, Thm.dest_arg ct) (* Apply cv to nth argument of t, counting from right and starting at 0. *) fun arg_backn_conv n cv ct = if n = 0 then Conv.arg_conv cv ct else Conv.fun_conv (arg_backn_conv (n-1) cv) ct (* Apply cv to nth argument of t, counting from left and starting at 0. *) fun argn_conv n cv ct = let val args_count = ct |> Thm.term_of |> dest_args |> length val _ = assert (n >= 0 andalso n < args_count) in arg_backn_conv (args_count - n - 1) cv ct end (* Given a head cterm f (function to be applied), and a list of equivalence theorems of arguments, produce an equivalent theorem for the overall term. *) fun comb_equiv (cf, arg_equivs) = Library.foldl (uncurry Thm.combination) (Thm.reflexive cf, arg_equivs) (* Retrive name of theorem. *) fun name_of_thm th = if Thm.has_name_hint th then Thm.get_name_hint th else raise Fail "name_of_thm: not found" (* Set the name of th to the name of ori_th, followed by suffix. *) fun update_name_of_thm ori_th suffix th = if Thm.has_name_hint ori_th then th |> Thm.put_name_hint (Thm.get_name_hint ori_th ^ suffix) else th val lhs_of = Thm.term_of o Thm.lhs_of val rhs_of = Thm.term_of o Thm.rhs_of fun assume_meta_eq thy (t1, t2) = Thm.assume (Thm.global_cterm_of thy (Logic.mk_equals (t1, t2))) fun assume_thm ctxt t = if type_of t <> propT then raise Fail "assume_thm: t is not of type prop" else Thm.assume (Thm.cterm_of ctxt t) (* Similar to Envir.subst_term. Apply an instantiation to a theorem. *) fun subst_thm_thy thy (tyinsts, insts) th = let fun process_tyenv (v, (S, T)) = ((v, S), Thm.global_ctyp_of thy T) val tys = map process_tyenv (Vartab.dest tyinsts) fun process_tenv (v, (T, u)) = ((v, Envir.subst_type tyinsts T), Thm.global_cterm_of thy u) val ts = map process_tenv (Vartab.dest insts) in th |> Drule.instantiate_normalize (TVars.make tys, Vars.make ts) end fun subst_thm ctxt (tyinsts, insts) th = subst_thm_thy (Proof_Context.theory_of ctxt) (tyinsts, insts) th fun send_first_to_hyps th = let val cprem = Thm.cprem_of th 1 in Thm.implies_elim th (Thm.assume cprem) end fun send_all_to_hyps th = let val _ = assert (forall (not o has_vars) (Thm.prems_of th)) "send_all_to_hyps: schematic variables in hyps." in funpow (Thm.nprems_of th) send_first_to_hyps th end (* Replace using subst the internal variables in th. This proceeds in several steps: first, pull any hypotheses of the theorem involving the replaced variables into statement of the theorem, perform the replacement (using forall_intr then forall_elim), finally return the hypotheses to their original place. *) fun subst_thm_atomic subst th = let val old_cts = map fst subst val old_ts = map Thm.term_of old_cts val new_cts = map snd subst val chyps = filter (fn ct => has_subterm old_ts (Thm.term_of ct)) (Thm.chyps_of th) in th |> fold Thm.implies_intr chyps |> fold Thm.forall_intr old_cts |> fold Thm.forall_elim (rev new_cts) |> funpow (length chyps) send_first_to_hyps end (* Substitution into terms used in auto2. Substitute types first and instantiate the types in the table of term instantiations. Also perform beta_norm at the end. *) fun subst_term_norm (tyinsts, insts) t = let fun inst_tenv tenv = tenv |> Vartab.dest |> map (fn (ixn, (T, v)) => (ixn, (Envir.subst_type tyinsts T, v))) |> Vartab.make in t |> Envir.subst_term_types tyinsts |> Envir.subst_term (tyinsts, inst_tenv insts) |> Envir.beta_norm end (* Apply the conversion cv to the statement of th, yielding the equivalent theorem. *) fun apply_to_thm cv th = let val eq = cv (Thm.cprop_of th) in if Thm.is_reflexive eq then th else Thm.equal_elim eq th end (* Given th of form A == B, get th' of form B == A. *) val meta_sym = Thm.symmetric (* Apply conv to rewrite the left hand side of th. *) fun apply_to_lhs cv th = let val eq = cv (Thm.lhs_of th) in if Thm.is_reflexive eq then th else Thm.transitive (meta_sym eq) th end (* Apply conv to rewrite the right hand side of th. *) fun apply_to_rhs cv th = let val eq = cv (Thm.rhs_of th) in if Thm.is_reflexive eq then th else Thm.transitive th eq end (* Using cv, rewrite the part of ct after stripping i premises. *) fun concl_conv_n i cv ct = if i = 0 then cv ct else (Conv.arg_conv (concl_conv_n (i-1) cv)) ct (* Rewrite part of ct after stripping all premises. *) fun concl_conv cv ct = case Thm.term_of ct of @{const Pure.imp} $ _ $ _ => Conv.arg_conv (concl_conv cv) ct | _ => cv ct (* Given a list of theorems A = B, B = C, etc., apply Thm.transitive to get equality between start and end. *) fun transitive_list ths = let fun rev_transitive btoc atob = let val (b, c) = btoc |> Thm.cprop_of |> Thm.dest_equals val (a, b') = atob |> Thm.cprop_of |> Thm.dest_equals in if b aconvc b' then if a aconvc b then btoc else if b aconvc c then atob else Thm.transitive atob btoc else let val _ = map (trace_thm_global "ths:") ths in raise Fail "transitive_list: intermediate does not agree" end end in fold rev_transitive (tl ths) (hd ths) end (* Skip to argument n times. For example, if applied to rewrite a proposition in implication form (==> or -->), it will skip the first n assumptions. *) fun skip_n_conv n cv = if n <= 0 then cv else Conv.arg_conv (skip_n_conv (n-1) cv) (* Given a term t, and pairs (a_i, eq_i), where a_i's are atomic subterms of t. Suppose the input is obtained by replacing each a_i by the left side of eq_i in t, obtain equality from t to the term obtained by replacing each a_i by the right side of eq_i in t. *) fun pattern_rewr_conv t eq_ths ct = case t of Bound _ => raise Fail "pattern_rewr_conv: bound variable." | Abs _ => raise Fail "pattern_rewr_conv: abs not supported." | _ $ _ => let val (f, arg) = Term.strip_comb t val (f', arg') = Drule.strip_comb ct val _ = assert (f aconv Thm.term_of f') "pattern_rewr_conv: input does not match pattern." val ths = map (fn (t, ct) => pattern_rewr_conv t eq_ths ct) (arg ~~ arg') in comb_equiv (f', ths) end | Const _ => let val _ = assert (t aconv Thm.term_of ct) "pattern_rewr_conv: input does not match pattern." in Conv.all_conv ct end | _ => (* Free and Var cases *) (case AList.lookup (op aconv) eq_ths t of NONE => Conv.all_conv ct | SOME eq_th => let val _ = assert (lhs_of eq_th aconv (Thm.term_of ct)) "pattern_rewr_conv: wrong substitution." in eq_th end) (* Given integer i, term b_i, and a term A = f(a_1, ..., a_n), produce the theorem a_i = b_i ==> A = f(a_1, ..., b_i, ..., a_n). *) fun eq_cong_th i bi A ctxt = let val thy = Proof_Context.theory_of ctxt val (cf, cargs) = Drule.strip_comb (Thm.cterm_of ctxt A) val _ = assert (i < length cargs) "eq_cong_th: i out of bounds." val ai = Thm.term_of (nth cargs i) val eq_i = assume_meta_eq thy (ai, bi) val eqs = map Thm.reflexive (take i cargs) @ [eq_i] @ map Thm.reflexive (drop (i + 1) cargs) val eq_A = comb_equiv (cf, eqs) in Thm.implies_intr (Thm.cprop_of eq_i) eq_A end (* Convert theorems of form !!x y. P x y into P ?x ?y (arbitrary number of quantifiers). *) fun forall_elim_sch th = case Thm.prop_of th of Const (@{const_name Pure.all}, _) $ Abs (x, T, _) => let val var_xs = map fst (Term.add_var_names (Thm.prop_of th) []) val x' = if member (op =) var_xs x then singleton (Name.variant_list var_xs) x else x val thy = Thm.theory_of_thm th in th |> Thm.forall_elim (Thm.global_cterm_of thy (Var ((x', 0), T))) |> forall_elim_sch end | _ => th (* Given P of function type, produce P == %x. P x. *) fun reverse_eta_conv ctxt ct = let val t = Thm.term_of ct val argT = Term.domain_type (fastype_of t) handle Match => raise CTERM ("reverse_eta_conv", [ct]) val rhs = Abs ("x", argT, t $ Bound 0) val eq_th = Thm.eta_conversion (Thm.cterm_of ctxt rhs) in meta_sym eq_th end (* Repeat cv exactly n times. *) fun repeat_n_conv n cv t = if n = 0 then Conv.all_conv t else (cv then_conv (repeat_n_conv (n-1) cv)) t (* Generic function for testing a conv. *) fun test_conv ctxt cv err_str (str1, str2) = let val (t1, t2) = (Proof_Context.read_term_pattern ctxt str1, Proof_Context.read_term_pattern ctxt str2) val th = cv (Thm.cterm_of ctxt t1) in if t1 aconv (lhs_of th) andalso t2 aconv (rhs_of th) then () else let val _ = trace_t ctxt "Input:" t1 val _ = trace_t ctxt "Expected:" t2 val _ = trace_t ctxt "Actual:" (Thm.prop_of th) in raise Fail err_str end end (* term_pat and typ_pat, from Isabelle Cookbook. *) val term_pat_setup = let - val parser = Args.context -- Scan.lift Args.embedded_inner_syntax + val parser = Args.context -- Scan.lift Parse.embedded_inner_syntax fun term_pat (ctxt, str) = str |> Proof_Context.read_term_pattern ctxt |> ML_Syntax.print_term |> ML_Syntax.atomic in ML_Antiquotation.inline @{binding "term_pat"} (parser >> term_pat) end val cterm_pat_setup = let - val parser = Args.context -- Scan.lift Args.embedded_inner_syntax + val parser = Args.context -- Scan.lift Parse.embedded_inner_syntax fun cterm_pat (ctxt, str) = str |> Proof_Context.read_term_pattern ctxt |> ML_Syntax.print_term |> ML_Syntax.atomic |> prefix "Thm.cterm_of ML_context" in ML_Antiquotation.value @{binding "cterm_pat"} (parser >> cterm_pat) end val type_pat_setup = let - val parser = Args.context -- Scan.lift Args.embedded_inner_syntax + val parser = Args.context -- Scan.lift Parse.embedded_inner_syntax fun typ_pat (ctxt, str) = let val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt in str |> Syntax.read_typ ctxt' |> ML_Syntax.print_typ |> ML_Syntax.atomic end in ML_Antiquotation.inline @{binding "typ_pat"} (parser >> typ_pat) end (* Time the given function f : unit -> 'a. *) fun timer (msg, f) = let val t_start = Timing.start () val res = f () val t_end = Timing.result t_start in (writeln (msg ^ (Timing.message t_end)); res) end (* When exception is shown when running function f : unit -> 'a, print stack trace. *) fun exn_trace f = Runtime.exn_trace f end (* structure Util. *) structure Basic_Util: BASIC_UTIL = Util open Basic_Util val _ = Theory.setup (Util.term_pat_setup) val _ = Theory.setup (Util.cterm_pat_setup) val _ = Theory.setup (Util.type_pat_setup) diff --git a/thys/Automatic_Refinement/Lib/Mk_Term_Antiquot.thy b/thys/Automatic_Refinement/Lib/Mk_Term_Antiquot.thy --- a/thys/Automatic_Refinement/Lib/Mk_Term_Antiquot.thy +++ b/thys/Automatic_Refinement/Lib/Mk_Term_Antiquot.thy @@ -1,212 +1,212 @@ section \Antiquotation to Build Terms\ theory Mk_Term_Antiquot imports Refine_Util_Bootstrap1 begin ML \ (* Antiquotation to generate a term from a template. This antiquotation takes a term with schematic variables, interprets the schematic variables as names of term-valued ML-variables and generates code to create the ML-level representation of the term with the schematics replaced by the ML-variables. All type variables in the term must be inferable from the types of the schematics. Limitations: * The type-inference is not complete, i.e., it may fail to detect some type-errors, resulting in untypable terms to be created. * Does not work if inserted terms contain loose bound variables (FIXME) TODO: * We could also provide explicit type variables Examples: See below *) local fun add_nv_tvars (Const (_,T)) l = Term.add_tvarsT T l | add_nv_tvars (Free (_,T)) l = Term.add_tvarsT T l | add_nv_tvars (Abs (_,T,t)) l = add_nv_tvars t (Term.add_tvarsT T l) | add_nv_tvars (t1$t2) l = add_nv_tvars t1 (add_nv_tvars t2 l) | add_nv_tvars _ l = l fun prepare env t ctxt = let val tvars = add_nv_tvars t [] val vars = Term.add_vars t [] val vtvars = fold (Term.add_tvarsT o #2) vars [] fun is_expl_tvar (n,i) = i=0 andalso String.isPrefix "'v_" n val expl_tvars = Term.add_tvars t [] |> filter (is_expl_tvar o #1) val spec_tvars = union (op =) vtvars expl_tvars val _ = subset (op =) (tvars, spec_tvars) orelse let val loose = subtract (op =) spec_tvars tvars |> map (TVar #> Syntax.pretty_typ ctxt) |> Pretty.commas |> Pretty.block val pretty_t = Syntax.pretty_term ctxt t val msg = Pretty.block [ Pretty.str "mk_term: Loose type variables in", Pretty.brk 1,pretty_t,Pretty.str ":",Pretty.brk 1,loose ] |> Pretty.string_of in error msg end val _ = fold (fn v as ((_,i),_) => fn () => if i<>0 then Pretty.block [ Pretty.str "mk_term: Variable indices must be zero:", Pretty.brk 1, Syntax.pretty_term ctxt (Var v) ] |> Pretty.string_of |> error else () ) vars () (* ARGH!!! "subtract eq a b" computes "b - a" *) val unused_tvars = subtract (op =) tvars vtvars |> map #1 (* val _ = tracing ("tvars: " ^ @{make_string} tvars) val _ = tracing ("vtvars: " ^ @{make_string} vtvars) val _ = tracing ("unused_tvars: " ^ @{make_string} unused_tvars) *) fun lin_type (TFree f) Ts = (TFree f, Ts) | lin_type (TVar (iname,S)) Ts = if is_expl_tvar iname orelse member (op =) Ts iname then (TVar (("_",0),S), Ts) else (TVar (iname,S), iname::Ts) | lin_type (Type (name,args)) Ts = let val (args,Ts) = map_fold lin_type args Ts in (Type (name,args),Ts) end; val (vars,_) = map_fold ( fn (iname,T) => fn Ts => let val (T,Ts) = lin_type T Ts in ((iname,T),Ts) end ) vars unused_tvars fun name_of_T (name,idx) = if is_expl_tvar (name,idx) then unprefix "'v_" name else "T_" ^ name ^ "_" ^ string_of_int idx local fun wrv (TVar (("_",_),_)) = "_" | wrv (TVar (iname,_)) = name_of_T iname | wrv (T as TFree _) = ML_Syntax.print_typ T | wrv (Type arg) = "Type " ^ ML_Syntax.print_pair ML_Syntax.print_string (ML_Syntax.print_list wrv) arg fun is_special (TVar _) = false | is_special _ = true fun mk_error_msg name T = Pretty.block [ Pretty.str ("mk_term type error: Argument for ?" ^ name ^ " does not match type"), Pretty.brk 1, Syntax.pretty_typ ctxt T ] |> Pretty.unformatted_string_of |> ML_Syntax.print_string fun pr_fastype name = case env of SOME env => "fastype_of1 (" ^ env ^ ", " ^ name ^ ")" | _ => "fastype_of " ^ name fun matcher ((name,_),T) rest = "case " ^ pr_fastype name ^ " of " ^ wrv T ^ " => (" ^ rest ^ ")" ^ ( if is_special T then "| _ => raise TERM ("^mk_error_msg name T^",["^name^"])" else "") in fun matchers [] rest = rest | matchers (v::vs) rest = matcher v (matchers vs rest) end local fun print_typ (Type arg) = "Type " ^ ML_Syntax.print_pair ML_Syntax.print_string (ML_Syntax.print_list print_typ) arg | print_typ (TFree arg) = "TFree " ^ ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_sort arg | print_typ (TVar (iname, _)) = name_of_T iname; fun print_term (Const arg) = "Const " ^ ML_Syntax.print_pair ML_Syntax.print_string print_typ arg | print_term (Free arg) = "Free " ^ ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_typ arg | print_term (Var ((name, _), _)) = name | print_term (Bound i) = "Bound " ^ ML_Syntax.print_int i | print_term (Abs (s, T, t)) = if String.isPrefix "v_" s then "Abs (" ^ unprefix "v_" s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")" else "Abs (" ^ ML_Syntax.print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")" | print_term (t1 $ t2) = ML_Syntax.atomic (print_term t1) ^ " $ " ^ ML_Syntax.atomic (print_term t2); in val et = print_term t val e = "(" ^ matchers vars et ^ ")" end in e end val read = Scan.lift (Scan.option (Args.name --| Args.colon)) -- - (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)) + (Args.context -- Scan.lift (Parse.position Parse.embedded_inner_syntax)) fun process (env,(ctxt,(raw_t,pos))) = let val t = Proof_Context.read_term_pattern ctxt raw_t in prepare env t ctxt end handle ERROR msg => error (msg ^ Position.here pos) in val mk_term_antiquot = read >> process end \ setup \ML_Antiquotation.inline @{binding mk_term} mk_term_antiquot\ subsection "Examples" ML_val \ (* The mk_term antiquotation can replace the omnipresent mk_xxx functions, and easily works with complex patterns *) fun mk_2elem_list a b = @{mk_term "[?a,?b]"} fun mk_compr s P = @{mk_term "{ x\?s. ?P x}"} val test1 = mk_2elem_list @{term "1::nat"} @{term "2::nat"} |> Thm.cterm_of @{context} val test2 = mk_compr @{term "{1,2,3::nat}"} @{term "(<) (2::nat)"} |> Thm.cterm_of @{context} val test3 = let val x = Bound 0 val env = [@{typ nat}] in @{mk_term env: "?x+?x"} end (* val test4 = let val x = Bound 0 val T = @{typ nat} in ctd here: Handle bounds below lambdas! @{mk_term "\x::?'v_T. ?x"} end *) \ end diff --git a/thys/Automatic_Refinement/Lib/Mpat_Antiquot.thy b/thys/Automatic_Refinement/Lib/Mpat_Antiquot.thy --- a/thys/Automatic_Refinement/Lib/Mpat_Antiquot.thy +++ b/thys/Automatic_Refinement/Lib/Mpat_Antiquot.thy @@ -1,255 +1,255 @@ section \Matching-Pattern Antiquotation\ theory Mpat_Antiquot imports Refine_Util_Bootstrap1 begin typedecl term_struct typedecl typ_struct typedecl sort definition mpaq_AS_PAT :: "'a \ 'a \ 'a" (infixl "AS\<^sub>p" 900) where "a AS\<^sub>p s \ a" definition mpaq_STRUCT :: "term_struct \ 'a" where "mpaq_STRUCT _ = undefined" abbreviation mpaq_AS_STRUCT :: "'a \ term_struct \ 'a" (infixl "AS\<^sub>s" 900) where "a AS\<^sub>s s \ a AS\<^sub>p mpaq_STRUCT s" consts mpaq_Const :: "string \ typ_struct \ term_struct" mpaq_Free :: "string \ typ_struct \ term_struct" mpaq_Var :: "string*nat \ typ_struct \ term_struct" mpaq_Bound :: "nat \ term_struct" mpaq_Abs :: "string \ typ_struct \ term_struct \ term_struct" mpaq_App :: "term_struct \ term_struct \ term_struct" (infixl "$$" 900) consts mpaq_TFree :: "string \ sort \ typ_struct" mpaq_TVar :: "string*nat \ sort \ typ_struct" mpaq_Type :: "string \ typ_struct list \ typ_struct" ML \ (* Antiquotation to generate a term-pattern in ML. Features: * Schematic term variables are translated to ML-variables of same name. * Non-dummy variables in lambda-abstractions are bound to variables of same name, and type of \x. t is bound to x_T * In (typs) mode, schematic type variables are translated if they start with 'v_, where the prefix is removed. Otherwise, types are completely ignored and translated to ML dummy pattern. * Dummy variables are translated to ML dummy patterns * Supports AS to define alternative pattern, and STRUCT to reflect term structure Limitations: * Non-linear patterns are not allowed, due to SML limitation. For term variables, it will result in an error. Type variables, however, are silently linearized and only the first occurrence is bound. * Indexes <>0 on term variables are not allowed. On type variables, such indexes are silently ignored. * Sorts are completely ignored * Due to the type-inference on patterns, only innermost types can be bound to names. * Patterns are not localized. Currently, we issue an error if pattern contains free variables. TODO: * We could also bind the type of a term-var, where the name for the type ML-var is encoded into the term-var name Examples: See below *) local fun replace_dummy' (Const (@{const_name Pure.dummy_pattern}, T)) i = (Var (("_dummy_", i), T), i + 1) | replace_dummy' (Abs (x, T, t)) i = let val (t', i') = replace_dummy' t i in (Abs (x, T, t'), i') end | replace_dummy' (t $ u) i = let val (t', i') = replace_dummy' t i; val (u', i'') = replace_dummy' u i'; in (t' $ u', i'') end | replace_dummy' a i = (a, i); fun prepare_dummies' ts = #1 (fold_map replace_dummy' ts 1); fun tcheck (Type (name,Ts)) tnames = let val (Ts,tnames) = map_fold tcheck Ts tnames in (Type (name,Ts),tnames) end | tcheck (TFree (name,_)) _ = error ("Pattern contains free type variable: " ^ name) | tcheck (TVar ((name,idx),S)) tnames = if String.isPrefix "'v_" name andalso not (member (op =) tnames name) then (TVar ((unprefix "'v_" name,idx),S),name::tnames) else (TVar (("_",0),S),tnames) fun vcheck (Const (n,T)) (vnames,tnames) = let val (T,tnames) = tcheck T tnames in (Const (n,T),(vnames,tnames)) end | vcheck (Free (n,_)) _ = error ("Pattern contains free variable: " ^ n) | vcheck (Var (("_dummy_",_),T)) (vnames,tnames) = let val (T,tnames) = tcheck T tnames in (Var (("_",0),T),(vnames,tnames)) end | vcheck (Var ((name,idx),T)) (vnames,tnames) = let val (T,tnames) = tcheck T tnames val _ = idx <> 0 andalso error ("Variable index greater zero: " ^ Term.string_of_vname (name,idx)) val _ = member (op =) vnames name andalso error ("Non-linear pattern: " ^ Term.string_of_vname (name,idx)) in (Var ((name,0),T),(name::vnames,tnames)) end | vcheck (Bound i) p = (Bound i,p) | vcheck (Abs ("uu_",T,t)) (vnames,tnames) = let val (T,tnames) = tcheck T tnames val (t,(vnames,tnames)) = vcheck t (vnames,tnames) in (Abs ("_",T,t),(vnames,tnames)) end | vcheck (Abs (x,T,t)) (vnames,tnames) = let val (T,tnames) = tcheck T tnames val (t,(vnames,tnames)) = vcheck t (vnames,tnames) in (Abs (x,T,t),(vnames,tnames)) end | vcheck (t1$t2) p = let val (t1,p) = vcheck t1 p val (t2,p) = vcheck t2 p in (t1$t2,p) end val read = Scan.lift (Args.mode "typs" ) - -- (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)) + -- (Args.context -- Scan.lift (Parse.position Parse.embedded_inner_syntax)) fun write (with_types, t) = let fun twr_aux (Type (name,Ts)) = "Type (" ^ ML_Syntax.print_string name ^ ", " ^ ML_Syntax.print_list twr_aux Ts ^ ")" | twr_aux (TFree (name,_)) = "TFree (" ^ ML_Syntax.print_string name ^ ", _)" | twr_aux (TVar ((name,_),_)) = name val twr = if with_types then twr_aux else K "_" fun s_string (Var ((name,_),_)) = name | s_string t = case try HOLogic.dest_string t of SOME s => ML_Syntax.print_string s | NONE => raise TERM ("Expected var or string literal",[t]) fun s_index (Var ((name,_),_)) = name | s_index t = case try HOLogic.dest_nat t of SOME n => ML_Syntax.print_int n | NONE => raise TERM ("Expected var or nat literal",[t]) fun s_indexname (Var ((name,_),_)) = name | s_indexname (Const (@{const_name Pair},_)$n$i) = "(" ^ s_string n ^ ", " ^ s_index i ^ ")" | s_indexname t = raise TERM ("Expected var or indexname-pair",[t]) fun s_typ (Var ((name,_),_)) = name | s_typ (Const(@{const_name "mpaq_TFree"},_)$name$typ) = "TFree (" ^ s_string name ^ "," ^ s_typ typ ^ ")" | s_typ (Const(@{const_name "mpaq_TVar"},_)$name$typ) = "TVar (" ^ s_indexname name ^ "," ^ s_typ typ ^ ")" | s_typ (Const(@{const_name "mpaq_Type"},_)$name$args) = "Type (" ^ s_string name ^ "," ^ s_args args ^ ")" | s_typ t = raise TERM ("Expected var or type structure",[t]) and s_args (Var ((name,_),_)) = name | s_args t = ( case try HOLogic.dest_list t of SOME l => ML_Syntax.print_list s_typ l | NONE => raise TERM ("Expected variable or type argument list",[t]) ) fun swr (Const(@{const_name "mpaq_Const"},_)$name$typ) = "Const (" ^ s_string name ^ ", " ^ s_typ typ ^ ")" | swr (Const(@{const_name "mpaq_Free"},_)$name$typ) = "Free (" ^ s_string name ^ ", " ^ s_typ typ ^ ")" | swr (Const(@{const_name "mpaq_Var"},_)$name$typ) = "Var (" ^ s_indexname name ^ ", " ^ s_typ typ ^ ")" | swr (Const(@{const_name "mpaq_Bound"},_)$idx) = "Bound " ^ s_index idx | swr (Const(@{const_name "mpaq_Abs"},_)$name$T$t) = "Abs (" ^ s_string name ^ ", " ^ s_typ T ^ ", " ^ swr t ^ ")" | swr (Const(@{const_name "mpaq_App"},_)$t1$t2) = "(" ^ swr t1 ^ ") $ (" ^ swr t2 ^ ")" | swr t = raise TERM ("Expected var or term structure",[t]) fun vwr (Const (name,T)) = "Const (" ^ ML_Syntax.print_string name ^ ", " ^ twr T ^ ")" | vwr (Var ((name,_),_)) = name | vwr (Free (name,T)) = "Free (" ^ name ^ ", " ^ twr T ^ ")" | vwr (Bound i) = "Bound " ^ ML_Syntax.print_int i | vwr (Abs ("_",T,t)) = "Abs (_," ^ twr T ^ "," ^ vwr t ^ ")" | vwr (Abs (x,T,t)) = "Abs (" ^ x ^ "," ^ x ^ "_T as " ^ twr T ^ "," ^ vwr t ^ ")" | vwr (Const(@{const_name mpaq_STRUCT},_)$t) = ( swr t ) | vwr (trm as Const(@{const_name "mpaq_AS_PAT"},_)$t$s) = ( case t of (Var ((name,_),_)) => name ^ " as (" ^ vwr s ^ ")" | _ => raise TERM ("_AS_ must have identifier on LHS",[trm]) ) | vwr (t1$t2) = "(" ^ vwr t1 ^ ") $ (" ^ vwr t2 ^ ")" val (t,_) = vcheck t ([],[]) val s = vwr t in "(" ^ s ^ ")" end fun process (with_types,(ctxt,(raw_t,pos))) = (let val ctxt' = Context.proof_map ( Syntax_Phases.term_check 90 "Prepare dummies" (K prepare_dummies') ) ctxt val t = Proof_Context.read_term_pattern ctxt' raw_t val res = write (with_types,t) in (*tracing res;*) res end handle ERROR msg => error (msg ^ Position.here pos) ) in val mpat_antiquot = read >> process end \ setup \ ML_Antiquotation.inline @{binding "mpat"} mpat_antiquot \ subsection \Examples\ ML_val \ fun dest_pair_singleton @{mpat "{(?a,_)}"} = (a) | dest_pair_singleton t = raise TERM ("dest_pair_singleton",[t]) fun dest_nat_pair_singleton @{mpat (typs) "{(?a::nat,?b::nat)}"} = (a,b) | dest_nat_pair_singleton t = raise TERM ("dest_nat_pair_singleton",[t]) fun dest_pair_singleton_T @{mpat (typs) "{(?a::_ \ ?'v_Ta,?b::?'v_Tb)}"} = ((a,Ta),(b,Tb)) | dest_pair_singleton_T t = raise TERM ("dest_pair_singleton_T",[t]) fun dest_pair_lambda @{mpat "{(\a _ _. ?Ta, \b. ?Tb)}"} = (a,a_T,b,b_T,Ta,Tb) | dest_pair_lambda t = raise TERM ("dest_pair_lambda",[t]) fun foo @{mpat "[?a,?b AS\<^sub>s mpaq_Bound ?i,?c AS\<^sub>p [?n]]"} = (a,b,i,c,n) | foo t = raise TERM ("foo",[t]) \ hide_type (open) term_struct typ_struct sort end 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,964 @@ 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.!!! Args.embedded_inner_syntax)) --| + (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 _ = 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/Collections/ICF/tools/ICF_Tools.thy b/thys/Collections/ICF/tools/ICF_Tools.thy --- a/thys/Collections/ICF/tools/ICF_Tools.thy +++ b/thys/Collections/ICF/tools/ICF_Tools.thy @@ -1,311 +1,311 @@ section \General ML-level tools\ theory ICF_Tools imports Main begin lemma meta_same_imp_rule: "(\PROP P; PROP P\ \ PROP Q) \ (PROP P \ PROP Q)" by rule (* TODO: Replace by distinct_prems_rl *) ML \ infix 0 ##; fun (f ## g) (a,b) = (f a, g b) signature ICF_TOOLS = sig (* Generic *) val gen_variant: (string -> bool) -> string -> string val map_option: ('a -> 'b) -> 'a option -> 'b option val parse_cpat: cterm context_parser val rename_cterm: (cterm * cterm) -> ctyp TVars.table * cterm Vars.table val renames_cterm: (cterm * cterm) -> bool val import_cterm: cterm -> Proof.context -> cterm * Proof.context val inst_meta_cong: Proof.context -> cterm -> thm (* val thms_from_main: string -> thm list val thm_from_main: string -> thm *) val sss_add: thm list -> Proof.context -> Proof.context val changed_conv: conv -> conv val repeat_top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv val rem_dup_prems: Proof.context -> thm -> thm (* Definition Theorems *) val dest_def_eq: term -> term * term val norm_def_thm: thm -> thm val dthm_lhs: thm -> term val dthm_rhs: thm -> term val dthm_params: thm -> term list val dthm_head: thm -> term val dt_lhs: term -> term val dt_rhs: term -> term val dt_params: term -> term list val dt_head: term -> term val chead_of: cterm -> cterm val chead_of_thm: thm -> cterm (* Simple definition: name\term, fixes variables *) val define_simple: string -> term -> local_theory -> ((term * thm) * local_theory) (* Wrapping stuff inside local theory context *) val wrap_lthy_result_global: (local_theory -> 'a * local_theory) -> (morphism -> 'a -> 'b) -> theory -> 'b * theory val wrap_lthy_global: (local_theory -> local_theory) -> theory -> theory val wrap_lthy_result_local: (local_theory -> 'a * local_theory) -> (morphism -> 'a -> 'b) -> local_theory -> 'b * local_theory val wrap_lthy_local: (local_theory -> local_theory) -> local_theory -> local_theory (* Wrapped versions of simple definition *) val define_simple_global: string -> term -> theory -> ((term * thm) * theory) val define_simple_local: string -> term -> local_theory -> ((term * thm) * local_theory) (* Revert abbreviations matching pattern (TODO/FIXME: HACK) *) val revert_abbrevs: string -> theory -> theory end; structure ICF_Tools: ICF_TOOLS = struct fun gen_variant decl s = let fun search s = if not (decl s) then s else search (Symbol.bump_string s); in if not (decl s) then s else search (Symbol.bump_init s) end; val parse_cpat = Args.context -- - Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, str) => + Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, str) => Proof_Context.read_term_pattern ctxt str |> Thm.cterm_of ctxt ); (* Renaming first-order match *) fun rename_cterm (ct1,ct2) = ( Thm.first_order_match (ct2,ct1); Thm.first_order_match (ct1,ct2)); val renames_cterm = can rename_cterm; fun import_cterm ct ctxt = let val (t', ctxt') = yield_singleton (Variable.import_terms true) (Thm.term_of ct) ctxt; val ct' = Thm.cterm_of ctxt' t'; in (ct', ctxt') end (* Get theorem by name, that is visible in HOL.Main. Moreover, the theory of this theorem will be HOL.Main, which is required to avoid non-trivial theory merges as they may occur when using thm-antiquotation. (cf. post https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00175.html on Isabelle mailing list) *)(* fun thms_from_main name = let val xthmref = Facts.named name; val thy = @{theory Main}; val name = Facts.ref_name xthmref |> Global_Theory.intern_fact thy; val name = case name of "_" => "Pure.asm_rl" | name => name; val fs = Global_Theory.facts_of thy; val thms = Facts.lookup (Context.Theory thy) fs name |> the |> #2 |> map (Thm.transfer thy); in thms end fun thm_from_main name = thms_from_main name |> Facts.the_single (name, Position.none) *) (* Unfold with simpset fun unfold_ss ss = let val simple_prover = SINGLE o (fn ss => ALLGOALS (resolve_tac (Raw_Simplifier.prems_of ss))); in Raw_Simplifier.rewrite_thm (true,false,false) simple_prover ss end; *) local fun sss_add_single thm ss = let val simps = Raw_Simplifier.dest_ss (simpset_of ss) |> #simps |> map #2; val ess = ss delsimps simps; val thm' = simplify ss thm; val new_simps = simps |> map (simplify (ess addsimps [thm'])); val ss' = ess addsimps (thm'::new_simps) in ss' end in val sss_add = fold sss_add_single end local open Conv; in fun changed_conv cnv = (fn (ct:cterm) => let val thm = cnv ct in if Thm.is_reflexive thm then raise THM ("changed_conv: Not changed",~1,[thm]) else thm end) fun repeat_top_sweep_conv cnv ctxt = repeat_conv (changed_conv (top_sweep_conv cnv ctxt)); end (* Remove duplicate premises (stable) *) fun rem_dup_prems ctxt thm = let val prems = Thm.prems_of thm; val perm = prems |> tag_list 0 |> map swap |> Termtab.make_list |> Termtab.dest |> map snd |> sort (int_ord o apply2 hd) |> flat; val thm' = Drule.rearrange_prems perm thm |> Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true @{thms meta_same_imp_rule}); in thm' end; fun dest_def_eq (Const (@{const_name Pure.eq},_)$l$r) = (l,r) | dest_def_eq (Const (@{const_name HOL.Trueprop},_) $(Const (@{const_name HOL.eq},_)$l$r)) = (l,r) | dest_def_eq t = raise TERM ("No definitional equation",[t]); fun norm_def_thm thm = case Thm.concl_of thm of (Const (@{const_name Pure.eq},_)$_$_) => thm | _ => thm RS eq_reflection; val dt_lhs = dest_def_eq #> fst; val dt_rhs = dest_def_eq #> snd; val dt_params = dt_lhs #> strip_comb #> snd; val dt_head = dt_lhs #> head_of; val dthm_lhs = Thm.concl_of #> dt_lhs; val dthm_rhs = Thm.concl_of #> dt_rhs; val dthm_params = Thm.concl_of #> dt_params; val dthm_head = Thm.concl_of #> dt_head; (* Head of function application (cterm) *) fun chead_of ct = case Thm.term_of ct of (_$_) => chead_of (Thm.dest_fun ct) | _ => ct; val chead_of_thm = norm_def_thm #> Thm.lhs_of #> chead_of; val meta_cong_rl = @{thm "eq_reflection"} OF @{thms "arg_cong"} OF @{thms "meta_eq_to_obj_eq"} fun inst_meta_cong ctxt ct = let val (ct, ctxt') = import_cterm ct ctxt; val mc_thm = meta_cong_rl; val fpat = mc_thm |> Thm.cprop_of |> Drule.strip_imp_concl |> Thm.dest_arg1 |> chead_of; val inst = infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of fpat)), ct)] mc_thm; val inst' = singleton (Variable.export ctxt' ctxt) inst; in inst' end (* Define name\rhs, generate _def theorem. *) fun define_simple name rhs lthy = let (* Import type variables *) val (rhs,lthy) = yield_singleton Variable.importT_terms rhs lthy; val ((ft,(_,def_thm)),lthy) = Local_Theory.define ((Binding.name name,NoSyn), ((Binding.name (Thm.def_name name),[]),rhs)) lthy; in ((ft,def_thm),lthy) end; fun wrap_lthy_result_global f rmap thy = let val lthy = Named_Target.theory_init thy; val (r,lthy) = f lthy; val (r,thy) = Local_Theory.exit_result_global rmap (r,lthy); in (r,thy) end fun wrap_lthy_global f = wrap_lthy_result_global (pair () o f) (K I) #> #2; fun wrap_lthy_result_local f rmap lthy = let val lthy = (snd o Local_Theory.begin_nested) lthy; val (r,lthy) = f lthy; val m = Local_Theory.target_morphism lthy; val lthy = Local_Theory.end_nested lthy; val r = rmap m r; in (r,lthy) end fun wrap_lthy_local f = wrap_lthy_result_local (pair () o f) (K I) #> #2; (* Define name\rhs, yielding constant *) fun define_simple_global name rhs thy = let val lthy = Named_Target.theory_init thy; val (r,lthy) = define_simple name rhs lthy; fun map_res m (t,thm) = (Morphism.term m t,Morphism.thm m thm); val (r,thy) = Local_Theory.exit_result_global (map_res) (r,lthy); in (r,thy) end; (* Define name\rhs, yielding constant *) fun define_simple_local name rhs lthy = let val lthy = (snd o Local_Theory.begin_nested) lthy; val (r,lthy) = define_simple name rhs lthy; val m = Local_Theory.target_morphism lthy; val lthy = Local_Theory.end_nested lthy; fun map_res m (t,thm) = (Morphism.term m t,Morphism.thm m thm); val (r,lthy) = (map_res m r,lthy); in (r,lthy) end; fun map_option _ NONE = NONE | map_option f (SOME a) = SOME (f a); fun revert_abbrevs mpat thy = let val ctxt = Proof_Context.init_global thy; val match_prefix = if Long_Name.is_qualified mpat then mpat else Long_Name.qualify (Context.theory_name thy) mpat; val {const_space, constants, ...} = Sign.consts_of thy |> Consts.dest; val names = Name_Space.extern_entries true ctxt const_space constants |> map_filter (fn ((name, _), (_, SOME _)) => if Long_Name.qualifier name = match_prefix then SOME name else NONE | _ => NONE) val _ = if null names then warning ("ICF_Tools.revert_abbrevs: No names with prefix: " ^ match_prefix) else (); in fold (Sign.revert_abbrev "") names thy end end; \ attribute_setup rem_dup_prems = \ Scan.succeed (Thm.rule_attribute [] (ICF_Tools.rem_dup_prems o Context.proof_of)) \ "Remove duplicate premises" method_setup dup_subgoals = \ Scan.succeed (fn ctxt => SIMPLE_METHOD (PRIMITIVE (ICF_Tools.rem_dup_prems ctxt))) \ "Remove duplicate subgoals" end diff --git a/thys/Constructor_Funs/constructor_funs.ML b/thys/Constructor_Funs/constructor_funs.ML --- a/thys/Constructor_Funs/constructor_funs.ML +++ b/thys/Constructor_Funs/constructor_funs.ML @@ -1,183 +1,183 @@ signature CONSTRUCTOR_FUNS = sig val mk_funs: Ctr_Sugar.ctr_sugar -> local_theory -> local_theory val mk_funs_typ: typ -> local_theory -> local_theory val mk_funs_cmd: string -> local_theory -> local_theory val enabled: bool Config.T val conv: Proof.context -> conv val constructor_funs_plugin: string val setup: theory -> theory end structure Constructor_Funs : CONSTRUCTOR_FUNS = struct val enabled = Attrib.setup_config_bool @{binding "constructor_funs"} (K false) structure Data = Generic_Data ( type T = term list * (int * thm) list * Symtab.set val empty = ([], [], Symtab.empty) fun merge ((ts1, unfolds1, s1), (ts2, unfolds2, s2)) = (ts1 @ ts2, unfolds1 @ unfolds2, Symtab.merge op = (s1, s2)) ) fun lenient_unvarify t = (* type variables in records are not schematic *) Logic.unvarify_global t handle TERM _ => t fun mk_funs {T, ctrs, ...} lthy = let val typ_name = fst (dest_Type T) fun mk_fun ctr lthy = let val (name, typ) = dest_Const (lenient_unvarify ctr) val (typs, _) = strip_type typ val len = length typs in if len > 0 then let val base_name = Long_Name.base_name name val binding = Binding.name base_name val args = Name.invent_names (Name.make_context [base_name]) Name.uu typs |> map Free val lhs = list_comb (Free (base_name, typ), args) val rhs = list_comb (Const (name, typ), args) val def = Logic.mk_equals (lhs, rhs) val ((term, (_, def_thm)), lthy') = Specification.definition NONE [] [] ((binding, []), def) lthy val unfold_thm = @{thm Pure.symmetric} OF [Local_Defs.abs_def_rule lthy' def_thm] in (SOME (term, (len, unfold_thm)), lthy') end else (NONE, lthy) end fun morph_unfold phi (len, thm) = (len, Morphism.thm phi thm) fun upd (ts', unfolds') = Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (fn (ts, unfolds, s) => (map (Morphism.term phi) ts' @ ts, map (morph_unfold phi) unfolds' @ unfolds, Symtab.update_new (typ_name, ()) s))) val exists = Symtab.defined (#3 (Data.get (Context.Proof lthy))) typ_name val warn = Pretty.separate "" [Syntax.pretty_typ lthy T, Pretty.str "already processed"] |> Pretty.block val _ = if exists then warning (Pretty.string_of warn) else () in if exists then lthy else (snd o Local_Theory.begin_nested) lthy |> Proof_Context.concealed |> Local_Theory.map_background_naming (Name_Space.mandatory_path typ_name #> Name_Space.mandatory_path "constructor_fun") |> fold_map mk_fun ctrs |>> map_filter I |>> split_list |-> upd |> Local_Theory.end_nested end fun mk_funs_typ typ lthy = mk_funs (the (Ctr_Sugar.ctr_sugar_of lthy (fst (dest_Type typ)))) lthy fun mk_funs_cmd s lthy = mk_funs_typ (Proof_Context.read_type_name {proper = true, strict = false} lthy s) lthy fun comb_conv ctxt cv1 cv2 ct = let val (f, xs) = strip_comb (Thm.term_of ct) val f = Thm.cterm_of ctxt f val xs = map (Thm.cterm_of ctxt) xs val f' = cv1 f val xs' = map cv2 xs in fold (fn x => fn f => Thm.combination f x) xs' f' end fun conv ctxt = let val (_, unfolds, _) = Data.get (Context.Proof ctxt) val unfolds = map (apsnd (Thm.transfer' ctxt)) unfolds fun full_conv ct = let val (_, xs) = strip_comb (Thm.term_of ct) val actual_len = length xs fun head_conv ct = let fun can_rewrite (len, thm) = Option.map (pair len) (try (Conv.rewr_conv thm) ct) val _ = get_first can_rewrite unfolds in case get_first can_rewrite unfolds of NONE => Conv.all_conv ct | SOME (target_len, thm) => if target_len = actual_len then Conv.all_conv ct else thm end in comb_conv ctxt head_conv full_conv ct end in full_conv end fun functrans ctxt thms = let val (consts, _, _) = Data.get (Context.Proof ctxt) val conv = Conv.arg_conv (conv ctxt) fun apply_conv thm = let val thm' = Conv.fconv_rule conv thm val prop = Thm.prop_of thm val head = Logic.dest_equals prop |> fst |> strip_comb |> fst val protected = exists (fn const => Pattern.matches (Proof_Context.theory_of ctxt) (const, head)) consts in if protected orelse Thm.prop_of thm aconv Thm.prop_of thm' then (false, thm) else (true, thm') end val (changeds, thms') = split_list (map apply_conv thms) in if exists I changeds then SOME thms' else NONE end val code_functrans = Code_Preproc.simple_functrans (fn ctxt => if Config.get ctxt enabled then functrans ctxt else K NONE) val constructor_funs_plugin = Plugin_Name.declare_setup @{binding constructor_funs} (** setup **) val _ = Outer_Syntax.local_theory @{command_keyword "constructor_funs"} "defines constructor functions for a datatype and sets up the code generator" - (Scan.repeat1 Args.embedded_inner_syntax >> fold mk_funs_cmd) + (Scan.repeat1 Parse.embedded_inner_syntax >> fold mk_funs_cmd) val setup = Code_Preproc.add_functrans ("constructor_funs", code_functrans) #> Ctr_Sugar.ctr_sugar_interpretation constructor_funs_plugin (mk_funs_typ o #T) end \ No newline at end of file diff --git a/thys/IMP2/lib/named_simpsets.ML b/thys/IMP2/lib/named_simpsets.ML --- a/thys/IMP2/lib/named_simpsets.ML +++ b/thys/IMP2/lib/named_simpsets.ML @@ -1,160 +1,160 @@ (* Named simpsets. Derived from named_theorems.ML *) signature NAMED_SIMPSETS = sig val get: Proof.context -> string -> simpset val clear: string -> Context.generic -> Context.generic val map: string -> (simpset -> simpset) -> Context.generic -> Context.generic val map_ctxt: string -> (Proof.context -> Proof.context) -> Context.generic -> Context.generic val put: string -> Proof.context -> Proof.context val get_all: Proof.context -> simpset Name_Space.table val add_simp: string -> thm -> Context.generic -> Context.generic val del_simp: string -> thm -> Context.generic -> Context.generic val add_cong: string -> thm -> Context.generic -> Context.generic val del_cong: string -> thm -> Context.generic -> Context.generic val add_split: string -> thm -> Context.generic -> Context.generic val del_split: string -> thm -> Context.generic -> Context.generic val add_attr: string -> attribute val del_attr: string -> attribute val add_cong_attr: string -> attribute val del_cong_attr: string -> attribute val add_split_attr: string -> attribute val del_split_attr: string -> attribute val check: Proof.context -> xstring * Position.T -> string val declare: binding -> simpset option -> local_theory -> local_theory val declare_cmd: binding -> (xstring * Position.T) option -> local_theory -> local_theory end; structure Named_Simpsets: NAMED_SIMPSETS = struct (* context data *) structure Data = Generic_Data ( type T = simpset Name_Space.table; val empty: T = Name_Space.empty_table "named-simpset"; val merge : T * T -> T = Name_Space.join_tables (K merge_ss); ); val content = Name_Space.get o Data.get val get = content o Context.Proof; val get_all = Data.get o Context.Proof fun put name ctxt = put_simpset (get ctxt name) ctxt fun map name f context = (content context name; Data.map (Name_Space.map_table_entry name f) context); fun map_ctxt name f context = map name (simpset_map (Context.proof_of context) f) context (* maintain content *) fun clear name = map_ctxt name clear_simpset; fun add_simp name thm = map_ctxt name (Simplifier.add_simp thm) fun del_simp name thm = map_ctxt name (Simplifier.del_simp thm) fun add_cong name thm = map_ctxt name (Simplifier.add_cong thm) fun del_cong name thm = map_ctxt name (Simplifier.del_cong thm) fun add_split name thm = map_ctxt name (Splitter.add_split thm) fun del_split name thm = map_ctxt name (Splitter.del_split thm) val add_attr = Thm.declaration_attribute o add_simp; val del_attr = Thm.declaration_attribute o del_simp; val add_cong_attr = Thm.declaration_attribute o add_cong; val del_cong_attr = Thm.declaration_attribute o del_cong; val add_split_attr = Thm.declaration_attribute o add_split; val del_split_attr = Thm.declaration_attribute o del_split; (* check *) fun check ctxt = let val context = Context.Proof ctxt in Name_Space.check context (Data.get context) #> #1 end (* declaration *) fun new_entry binding init = let fun decl _ context = let val sstab = Data.get context val ss = the_default (Raw_Simplifier.clear_simpset (Context.proof_of context) |> simpset_of) init val (_,sstab) = Name_Space.define context true (binding,ss) sstab in Data.put sstab context end in Local_Theory.declaration {syntax=false, pervasive=true} decl end fun declare binding init lthy = let val lthy' = lthy |> new_entry binding init in (lthy') end; fun declare_cmd binding init_src lthy = let val init = Option.map (get lthy o check lthy) init_src in declare binding init lthy end val named_simpset_attr = - (Args.context -- Scan.lift (Parse.position Args.embedded)) + (Args.context -- Scan.lift (Parse.position Parse.embedded)) :|-- (fn (ctxt,raw_binding) => let val name = check ctxt raw_binding in (Scan.lift (Args.$$$ "simp") |-- Attrib.add_del (add_attr name) (del_attr name)) || (Scan.lift (Args.$$$ "cong") |-- Attrib.add_del (add_cong_attr name) (del_cong_attr name)) || (Scan.lift (Args.$$$ "split") |-- Attrib.add_del (add_split_attr name) (del_split_attr name)) || Attrib.add_del (add_attr name) (del_attr name) end ) val _ = Theory.setup (Attrib.setup \<^binding>\named_ss\ named_simpset_attr "Modify named simpsets") val put_named_simpset_attr = - (Args.context -- Scan.lift (Parse.position Args.embedded)) >> (fn (ctxt,raw_binding) => let + (Args.context -- Scan.lift (Parse.position Parse.embedded)) >> (fn (ctxt,raw_binding) => let val name = check ctxt raw_binding val attr = Thm.declaration_attribute (fn _ => Context.map_proof (put name)) in attr end) val _ = Theory.setup (Attrib.setup \<^binding>\put_named_ss\ put_named_simpset_attr "Activate named simpset") (* ML antiquotation *) val _ = Theory.setup (ML_Antiquotation.inline \<^binding>\named_simpset\ - (Args.context -- Scan.lift (Parse.position Args.embedded) >> + (Args.context -- Scan.lift (Parse.position Parse.embedded) >> (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name)))); end; diff --git a/thys/Lazy_Case/lazy_case.ML b/thys/Lazy_Case/lazy_case.ML --- a/thys/Lazy_Case/lazy_case.ML +++ b/thys/Lazy_Case/lazy_case.ML @@ -1,192 +1,192 @@ signature LAZY_CASE = sig val lazify: Ctr_Sugar.ctr_sugar -> local_theory -> local_theory val lazify_typ: typ -> local_theory -> local_theory val lazify_cmd: string -> local_theory -> local_theory val lazy_case_plugin: string val setup: theory -> theory end structure Lazy_Case : LAZY_CASE = struct structure Data = Generic_Data ( type T = Symtab.set val empty = Symtab.empty val merge = Symtab.merge op = ) fun init [] = error "empty list" | init [_] = [] | init (x :: xs) = x :: init xs fun lazify {T, casex, ctrs, case_thms, case_cong, ...} lthy = let val is_fun = can dest_funT val typ_name = fst (dest_Type T) val len = length ctrs val idxs = 0 upto len - 1 val (name, typ) = dest_Const casex ||> Logic.unvarifyT_global val (typs, _) = strip_type typ val exists = Symtab.defined (Data.get (Context.Proof lthy)) typ_name val warn = Pretty.separate "" [Syntax.pretty_typ lthy T, Pretty.str "already lazified"] |> Pretty.block val _ = if exists then warning (Pretty.string_of warn) else () in (* for records, casex is the dummy pattern *) if Term.is_dummy_pattern casex orelse forall is_fun (init typs) orelse exists then lthy else let val arg_typs = init typs fun apply_to_unit typ idx = if is_fun typ then (typ, Bound idx) else (@{typ unit} --> typ, Bound idx $ @{term "()"}) val (arg_typs', args) = split_list (map2 apply_to_unit arg_typs (rev idxs)) val def = list_comb (Const (name, typ), args) |> fold_rev Term.abs (map (pair "c") arg_typs') val binding = Binding.name "case_lazy" val ((term, thm), (lthy', lthy)) = (snd o Local_Theory.begin_nested) lthy |> Proof_Context.concealed |> Local_Theory.map_background_naming (Name_Space.mandatory_path typ_name) |> Local_Theory.define ((binding, NoSyn), ((Thm.def_binding binding, []), def)) |>> apsnd snd ||> `Local_Theory.end_nested val phi = Proof_Context.export_morphism lthy lthy' val thm' = Morphism.thm phi thm val term' = Logic.unvarify_global (Morphism.term phi term) fun defs_tac ctxt idx = Local_Defs.unfold_tac ctxt [thm', nth case_thms idx] THEN HEADGOAL (resolve_tac ctxt @{thms refl}) val frees = fastype_of term' |> strip_type |> fst |> init val frees_f = Name.invent_names Name.context "f0" frees val frees_g = Name.invent_names Name.context "g0" frees val fs = map Free frees_f val gs = map Free frees_g fun mk_def_goal ctr idx = let val (name, len) = dest_Const ctr ||> strip_type ||> fst ||> length val frees = Name.invent Name.context "p0" len val args = map (Free o rpair dummyT) frees val ctr_val = list_comb (Const (name, dummyT), args) val lhs = list_comb (term', fs) $ ctr_val val rhs = if len = 0 then nth fs idx $ @{term "()"} else list_comb (nth fs idx, args) in (frees, HOLogic.mk_Trueprop (Syntax.check_term lthy' (HOLogic.mk_eq (lhs, rhs)))) end fun prove_defs (frees', goal) idx = Goal.prove_future lthy' (map fst frees_f @ frees') [] goal (fn {context, ...} => defs_tac context idx) val def_thms = map2 prove_defs (map2 mk_def_goal ctrs idxs) idxs val frees = Name.invent_names Name.context "q0" arg_typs val unfold_goal = let val lhs = list_comb (Const (name, typ), map Free frees) fun mk_abs (name, typ) = if is_fun typ then Free (name, typ) else Abs ("u", @{typ unit}, Free (name, typ)) val rhs = list_comb (Const (fst (dest_Const term'), dummyT), map mk_abs frees) in HOLogic.mk_Trueprop (Syntax.check_term lthy' (HOLogic.mk_eq (lhs, rhs))) end fun unfold_tac ctxt = Local_Defs.unfold_tac ctxt [thm'] THEN HEADGOAL (resolve_tac ctxt @{thms refl}) val unfold_thm = Goal.prove_future lthy' (map fst frees) [] unfold_goal (fn {context, ...} => unfold_tac context) fun mk_cong_prem t ctr (f, g) = let (* FIXME get rid of dummyT here *) fun mk_all t = Logic.all_const dummyT $ Abs ("", dummyT, t) val len = dest_Const ctr |> snd |> strip_type |> fst |> length val args = map Bound (len - 1 downto 0) val ctr_val = list_comb (Logic.unvarify_global ctr, args) val args' = if len = 0 then [Bound 0] else args val lhs = list_comb (f, args') val rhs = list_comb (g, args') val concl = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, ctr_val)) in fold (K mk_all) args' (Logic.mk_implies (prem, concl)) end val cong_goal = let val t1 = Free ("t1", Logic.unvarifyT_global T) val t2 = Free ("t2", Logic.unvarifyT_global T) val prems = HOLogic.mk_Trueprop (HOLogic.mk_eq (t1, t2)) :: map2 (mk_cong_prem t2) ctrs (fs ~~ gs) val lhs = list_comb (term', fs) $ t1 val rhs = list_comb (term', gs) $ t2 val concl = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) in Logic.list_implies (prems, concl) |> Syntax.check_term lthy' end fun cong_tac ctxt = Local_Defs.unfold_tac ctxt [thm'] THEN HEADGOAL (eresolve_tac ctxt [case_cong]) THEN ALLGOALS (ctxt |> Subgoal.FOCUS (fn {context = ctxt, prems, ...} => HEADGOAL (resolve_tac ctxt prems THEN' resolve_tac ctxt prems))) val cong_thm = Goal.prove_future lthy' ("t1" :: "t2" :: map fst frees_f @ map fst frees_g) [] cong_goal (fn {context, ...} => cong_tac context) val upd = Data.map (Symtab.update_new (typ_name, ())) in lthy' |> Local_Theory.note ((Binding.empty, @{attributes [code]}), def_thms) |> snd |> Local_Theory.note ((Binding.empty, @{attributes [code_unfold]}), [unfold_thm]) |> snd |> Local_Theory.note ((Binding.empty, @{attributes [fundef_cong]}), [cong_thm]) |> snd |> Local_Theory.declaration {syntax = false, pervasive = true} (K upd) end end fun lazify_typ typ lthy = lazify (the (Ctr_Sugar.ctr_sugar_of lthy (fst (dest_Type typ)))) lthy fun lazify_cmd s lthy = lazify_typ (Proof_Context.read_type_name {proper = true, strict = false} lthy s) lthy val lazy_case_plugin = Plugin_Name.declare_setup @{binding lazy_case} (** setup **) val _ = Outer_Syntax.local_theory @{command_keyword "lazify"} "defines a lazy case constant and sets up the code generator" - (Scan.repeat1 Args.embedded_inner_syntax >> fold lazify_cmd) + (Scan.repeat1 Parse.embedded_inner_syntax >> fold lazify_cmd) val setup = Ctr_Sugar.ctr_sugar_interpretation lazy_case_plugin (lazify_typ o #T) end \ No newline at end of file diff --git a/thys/Refine_Monadic/Refine_Automation.thy b/thys/Refine_Monadic/Refine_Automation.thy --- a/thys/Refine_Monadic/Refine_Automation.thy +++ b/thys/Refine_Monadic/Refine_Automation.thy @@ -1,555 +1,555 @@ section "More Automation" theory Refine_Automation imports Refine_Basic Refine_Transfer keywords "concrete_definition" :: thy_decl and "prepare_code_thms" :: thy_decl and "uses" begin text \ This theory provides a tool for extracting definitions from terms, and for generating code equations for recursion combinators. \ ML \ signature REFINE_AUTOMATION = sig type extraction = { pattern: term, (* Pattern to be defined as own constant *) gen_thm: thm, (* Code eq generator: [| c==rhs; ... |] ==> c == ... *) gen_tac: local_theory -> tactic' (* Solves remaining premises of gen_thm *) } val extract_as_def: (string * typ) list -> string -> term -> local_theory -> ((term * thm) * local_theory) val extract_recursion_eqs: extraction list -> string -> thm -> local_theory -> local_theory val add_extraction: string -> extraction -> theory -> theory val prepare_code_thms_cmd: string list -> thm -> local_theory -> local_theory val define_concrete_fun: extraction list option -> binding -> Token.src list -> indexname list -> thm -> cterm list -> local_theory -> (thm * thm) * local_theory val mk_qualified: string -> bstring -> binding val prepare_cd_pattern: Proof.context -> cterm -> cterm val add_cd_pattern: cterm -> Context.generic -> Context.generic val del_cd_pattern: cterm -> Context.generic -> Context.generic val get_cd_patterns: Proof.context -> cterm list val add_vc_rec_thm: thm -> Context.generic -> Context.generic val del_vc_rec_thm: thm -> Context.generic -> Context.generic val get_vc_rec_thms: Proof.context -> thm list val add_vc_solve_thm: thm -> Context.generic -> Context.generic val del_vc_solve_thm: thm -> Context.generic -> Context.generic val get_vc_solve_thms: Proof.context -> thm list val vc_solve_tac: Proof.context -> bool -> tactic' val vc_solve_modifiers: Method.modifier parser list val setup: theory -> theory end structure Refine_Automation :REFINE_AUTOMATION = struct type extraction = { pattern: term, (* Pattern to be defined as own constant *) gen_thm: thm, (* Code eq generator: [| c==rhs; ... |] ==> c == ... *) gen_tac: local_theory -> tactic' (* Solves remaining premises of gen_thm *) } structure extractions = Generic_Data ( type T = extraction list Symtab.table val empty = Symtab.empty val merge = Symtab.merge_list ((op =) o apply2 #pattern) ) fun add_extraction name ex = Context.theory_map (extractions.map ( Symtab.update_list ((op =) o apply2 #pattern) (name,ex))) (* Define new constant name for subterm t in context bnd. Returns replacement for t using the new constant and definition theorem. *) fun extract_as_def bnd name t lthy = let val loose = rev (loose_bnos t); val rnames = #1 (Variable.names_of lthy |> fold_map (Name.variant o #1) bnd); val rfrees = map (fn (name,(_,typ)) => Free (name,typ)) (rnames ~~ bnd); val t' = subst_bounds (rfrees,t); val params = map Bound (rev loose); val param_vars = (Library.foldl (fn (l,i) => nth rfrees i :: l) ([],loose)); val param_types = map fastype_of param_vars; val def_t = Logic.mk_equals (list_comb (Free (name,param_types ---> fastype_of t'),param_vars),t'); val ((lhs_t,(_,def_thm)),lthy) = Specification.definition NONE [] [] (Binding.empty_atts,def_t) lthy; (*val _ = tracing "xxxx";*) val app_t = list_comb (lhs_t, params); in ((app_t,def_thm),lthy) end; fun mk_qualified basename q = Binding.qualify true basename (Binding.name q); fun extract_recursion_eqs exs basename orig_def_thm lthy = let val thy = Proof_Context.theory_of lthy val pat_net : extraction Item_Net.T = Item_Net.init ((op =) o apply2 #pattern) (fn {pattern, ...} => [pattern]) |> fold Item_Net.update exs local fun tr env t ctx = let (* Recurse for subterms *) val (t,ctx) = case t of t1$t2 => let val (t1,ctx) = tr env t1 ctx val (t2,ctx) = tr env t2 ctx in (t1$t2,ctx) end | Abs (x,T,t) => let val (t',ctx) = tr ((x,T)::env) t ctx in (Abs (x,T,t'),ctx) end | _ => (t,ctx) (* Check if we match a pattern *) val ex = Item_Net.retrieve_matching pat_net t |> get_first (fn ex => case try (Pattern.first_order_match thy (#pattern ex,t)) (Vartab.empty,Vartab.empty) of NONE => NONE | SOME _ => SOME ex ) in case ex of NONE => (t,ctx) | SOME ex => let (* Extract as new constant *) val (idx,defs,lthy) = ctx val name = (basename ^ "_" ^ string_of_int idx) val ((t,def_thm),lthy) = extract_as_def env name t lthy val ctx = (idx+1,(def_thm,ex)::defs,lthy) in (t,ctx) end end in fun transform t lthy = let val (t,(_,defs,lthy)) = tr [] t (0,[],lthy) in ((t,defs),lthy) end end (* Import theorem and extract RHS *) val ((_,orig_def_thm'),lthy) = yield_singleton2 (Variable.import true) orig_def_thm lthy; val (lhs,rhs) = orig_def_thm' |> Thm.prop_of |> Logic.dest_equals; (* Transform RHS, generating new constants *) val ((rhs',defs),lthy) = transform rhs lthy; val def_thms = map #1 defs (* Register definitions of generated constants *) val (_,lthy) = Local_Theory.note ((mk_qualified basename "defs",[]),def_thms) lthy; (* Obtain new def_thm *) val def_unfold_ss = put_simpset HOL_basic_ss lthy addsimps (orig_def_thm::def_thms) val new_def_thm = Goal.prove_internal lthy [] (Logic.mk_equals (lhs,rhs') |> Thm.cterm_of lthy) (K (simp_tac def_unfold_ss 1)) (* Obtain new theorem by folding with defs of generated constants *) (* TODO: Maybe cleaner to generate eq-thm and prove by "unfold, refl" *) (*val new_def_thm = Library.foldr (fn (dt,t) => Local_Defs.fold lthy [dt] t) (def_thms,orig_def_thm');*) (* Prepare code equations *) fun mk_code_thm lthy (def_thm,{gen_thm, gen_tac, ...}) = let val ((_,def_thm),lthy') = yield_singleton2 (Variable.import true) def_thm lthy; val thm = def_thm RS gen_thm; val tac = SOLVED' (gen_tac lthy') ORELSE' (simp_tac def_unfold_ss THEN' gen_tac lthy') val thm = the (SINGLE (ALLGOALS tac) thm); val thm = singleton (Variable.export lthy' lthy) thm; in thm end; val code_thms = map (mk_code_thm lthy) defs; val _ = if forall Thm.no_prems code_thms then () else warning "Unresolved premises in code theorems" val (_,lthy) = Local_Theory.note ((mk_qualified basename "code",@{attributes [code]}),new_def_thm::code_thms) lthy; in lthy end; fun prepare_code_thms_cmd names thm lthy = let fun name_of (Const (n,_)) = n | name_of (Free (n,_)) = n | name_of _ = raise (THM ("No definitional theorem",0,[thm])); val (lhs,_) = thm |> Thm.prop_of |> Logic.dest_equals; val basename = lhs |> strip_comb |> #1 |> name_of |> Long_Name.base_name; val exs_tab = extractions.get (Context.Proof lthy) fun get_exs name = case Symtab.lookup exs_tab name of NONE => error ("No such extraction mode: " ^ name) | SOME exs => exs val exs = case names of [] => Symtab.dest_list exs_tab |> map #2 | _ => map get_exs names |> flat val _ = case exs of [] => error "No extraction patterns selected" | _ => () val lthy = extract_recursion_eqs exs basename thm lthy in lthy end; fun extract_concrete_fun _ [] concl = raise TERM ("Conclusion does not match any extraction pattern",[concl]) | extract_concrete_fun thy (pat::pats) concl = ( case Refine_Util.fo_matchp thy pat concl of NONE => extract_concrete_fun thy pats concl | SOME [t] => t | SOME (t::_) => ( warning ("concrete_definition: Pattern has multiple holes, taking " ^ "first one: " ^ @{make_string} pat ); t) | _ => (warning ("concrete_definition: Ignoring invalid pattern " ^ @{make_string} pat); extract_concrete_fun thy pats concl) ) (* Define concrete function from refinement lemma *) fun define_concrete_fun gen_code fun_name attribs_raw param_names thm pats (orig_lthy:local_theory) = let val lthy = orig_lthy; val (((_,inst),thm'),lthy) = yield_singleton2 (Variable.import true) thm lthy; val concl = thm' |> Thm.concl_of (*val ((typ_subst,term_subst),lthy) = Variable.import_inst true [concl] lthy; val concl = Term_Subst.instantiate (typ_subst,term_subst) concl; *) val term_subst = build (inst |> Vars.fold (cons o apsnd Thm.term_of)) val param_terms = map (fn name => case AList.lookup (fn (n,v) => n = #1 v) term_subst name of NONE => raise TERM ("No such variable: " ^Term.string_of_vname name,[concl]) | SOME t => t ) param_names; val f_term = extract_concrete_fun (Proof_Context.theory_of lthy) pats concl; val lhs_type = map Term.fastype_of param_terms ---> Term.fastype_of f_term; val lhs_term = list_comb ((Free (Binding.name_of fun_name,lhs_type)),param_terms); val def_term = Logic.mk_equals (lhs_term,f_term) |> fold Logic.all param_terms; val attribs = map (Attrib.check_src lthy) attribs_raw; val ((_,(_,def_thm)),lthy) = Specification.definition (SOME (fun_name,NONE,Mixfix.NoSyn)) [] [] ((Binding.empty,attribs),def_term) lthy; val folded_thm = Local_Defs.fold lthy [def_thm] thm'; val (_,lthy) = Local_Theory.note ((mk_qualified (Binding.name_of fun_name) "refine",[]),[folded_thm]) lthy; val lthy = case gen_code of NONE => lthy | SOME modes => extract_recursion_eqs modes (Binding.name_of fun_name) def_thm lthy in ((def_thm,folded_thm),lthy) end; val cd_pat_eq = apply2 (Thm.term_of #> Refine_Util.anorm_term) #> (op aconv) structure cd_patterns = Generic_Data ( type T = cterm list val empty = [] val merge = merge cd_pat_eq ) fun prepare_cd_pattern ctxt pat = case Thm.term_of pat |> fastype_of of @{typ bool} => Thm.term_of pat |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt | _ => pat fun add_cd_pattern pat context = cd_patterns.map (insert cd_pat_eq (prepare_cd_pattern (Context.proof_of context) pat)) context fun del_cd_pattern pat context = cd_patterns.map (remove cd_pat_eq (prepare_cd_pattern (Context.proof_of context) pat)) context val get_cd_patterns = cd_patterns.get o Context.Proof structure rec_thms = Named_Thms ( val name = @{binding vcs_rec} val description = "VC-Solver: Recursive intro rules" ) structure solve_thms = Named_Thms ( val name = @{binding vcs_solve} val description = "VC-Solver: Solve rules" ) val add_vc_rec_thm = rec_thms.add_thm val del_vc_rec_thm = rec_thms.del_thm val get_vc_rec_thms = rec_thms.get val add_vc_solve_thm = solve_thms.add_thm val del_vc_solve_thm = solve_thms.del_thm val get_vc_solve_thms = solve_thms.get val rec_modifiers = [ Args.$$$ "rec" -- Scan.option Args.add -- Args.colon >> K (Method.modifier rec_thms.add \<^here>), Args.$$$ "rec" -- Scan.option Args.del -- Args.colon >> K (Method.modifier rec_thms.del \<^here>) ]; val solve_modifiers = [ Args.$$$ "solve" -- Scan.option Args.add -- Args.colon >> K (Method.modifier solve_thms.add \<^here>), Args.$$$ "solve" -- Scan.option Args.del -- Args.colon >> K (Method.modifier solve_thms.del \<^here>) ]; val vc_solve_modifiers = clasimp_modifiers @ rec_modifiers @ solve_modifiers; fun vc_solve_tac ctxt no_pre = let val rthms = rec_thms.get ctxt val sthms = solve_thms.get ctxt val pre_tac = if no_pre then K all_tac else clarsimp_tac ctxt val tac = SELECT_GOAL (auto_tac ctxt) in TRY o pre_tac THEN_ALL_NEW_FWD (TRY o REPEAT_ALL_NEW_FWD (resolve_tac ctxt rthms)) THEN_ALL_NEW_FWD (TRY o SOLVED' (resolve_tac ctxt sthms THEN_ALL_NEW_FWD tac)) end val setup = I #> rec_thms.setup #> solve_thms.setup end; \ setup Refine_Automation.setup setup \ let fun parse_cpat cxt = let - val (t, (context, tks)) = Scan.lift Args.embedded_inner_syntax cxt + val (t, (context, tks)) = Scan.lift Parse.embedded_inner_syntax cxt val ctxt = Context.proof_of context val t = Proof_Context.read_term_pattern ctxt t in (Thm.cterm_of ctxt t, (context, tks)) end fun do_p f = Scan.repeat1 parse_cpat >> (fn pats => Thm.declaration_attribute (K (fold f pats))) in Attrib.setup @{binding "cd_patterns"} ( Scan.lift Args.add |-- do_p Refine_Automation.add_cd_pattern || Scan.lift Args.del |-- do_p Refine_Automation.del_cd_pattern || do_p Refine_Automation.add_cd_pattern ) "Add/delete concrete_definition pattern" end \ (* Command setup *) (* TODO: Folding of .refine-lemma seems not to work, if the function has parameters on which it does not depend *) ML \Outer_Syntax.local_theory @{command_keyword concrete_definition} "Define function from refinement theorem" (Parse.binding -- Parse.opt_attribs -- Scan.optional (@{keyword "for"} |-- Scan.repeat1 Args.var) [] --| @{keyword "uses"} -- Parse.thm - -- Scan.optional (@{keyword "is"} |-- Scan.repeat1 Args.embedded_inner_syntax) [] + -- Scan.optional (@{keyword "is"} |-- Scan.repeat1 Parse.embedded_inner_syntax) [] >> (fn ((((name,attribs),params),raw_thm),pats) => fn lthy => let val thm = case Attrib.eval_thms lthy [raw_thm] of [thm] => thm | _ => error "Expecting exactly one theorem"; val pats = case pats of [] => Refine_Automation.get_cd_patterns lthy | l => map (Proof_Context.read_term_pattern lthy #> Thm.cterm_of lthy #> Refine_Automation.prepare_cd_pattern lthy) l in Refine_Automation.define_concrete_fun NONE name attribs params thm pats lthy |> snd end)) \ text \ Command: \concrete_definition name [attribs] for params uses thm is patterns\ where \attribs\, \for\, and \is\-parts are optional. Declares a new constant \name\ by matching the theorem \thm\ against a pattern. If the \for\ clause is given, it lists variables in the theorem, and thus determines the order of parameters of the defined constant. Otherwise, parameters will be in order of occurrence. If the \is\ clause is given, it lists patterns. The conclusion of the theorem will be matched against each of these patterns. For the first matching pattern, the constant will be declared to be the term that matches the first non-dummy variable of the pattern. If no \is\-clause is specified, the default patterns will be tried. Attribute: \cd_patterns pats\. Declaration attribute. Declares default patterns for the \concrete_definition\ command. \ declare [[ cd_patterns "(?f,_)\_"]] declare [[ cd_patterns "RETURN ?f \ _" "nres_of ?f \ _"]] declare [[ cd_patterns "(RETURN ?f,_)\_" "(nres_of ?f,_)\_"]] declare [[ cd_patterns "_ = ?f" "_ == ?f" ]] ML \ let val modes = (Scan.optional (@{keyword "("} |-- Parse.list1 Parse.name --| @{keyword ")"}) []) in Outer_Syntax.local_theory @{command_keyword prepare_code_thms} "Refinement framework: Prepare theorems for code generation" (modes -- Parse.thms1 >> (fn (modes,raw_thms) => fn lthy => let val thms = Attrib.eval_thms lthy raw_thms in fold (Refine_Automation.prepare_code_thms_cmd modes) thms lthy end) ) end \ text \ Command: \prepare_code_thms (modes) thm\ where the \(mode)\-part is optional. Set up code-equations for recursions in constant defined by \thm\. The optional \modes\ is a comma-separated list of extraction modes. \ lemma gen_code_thm_RECT: fixes x assumes D: "f \ RECT B" assumes M: "trimono B" shows "f x \ B f x" unfolding D apply (subst RECT_unfold) by (rule M) lemma gen_code_thm_REC: fixes x assumes D: "f \ REC B" assumes M: "trimono B" shows "f x \ B f x" unfolding D apply (subst REC_unfold) by (rule M) setup \ Refine_Automation.add_extraction "nres" { pattern = Logic.varify_global @{term "REC x"}, gen_thm = @{thm gen_code_thm_REC}, gen_tac = Refine_Mono_Prover.mono_tac } #> Refine_Automation.add_extraction "nres" { pattern = Logic.varify_global @{term "RECT x"}, gen_thm = @{thm gen_code_thm_RECT}, gen_tac = Refine_Mono_Prover.mono_tac } \ text \ Method \vc_solve (no_pre) clasimp_modifiers rec (add/del): ... solve (add/del): ...\ Named theorems \vcs_rec\ and \vcs_solve\. This method is specialized to solve verification conditions. It first clarsimps all goals, then it tries to apply a set of safe introduction rules (\vcs_rec\, \rec add\). Finally, it applies introduction rules (\vcs_solve\, \solve add\) and tries to discharge all emerging subgoals by auto. If this does not succeed, it backtracks over the application of the solve-rule. \ method_setup vc_solve = \Scan.lift (Args.mode "nopre") --| Method.sections Refine_Automation.vc_solve_modifiers >> (fn (nopre) => fn ctxt => SIMPLE_METHOD ( CHANGED (ALLGOALS (Refine_Automation.vc_solve_tac ctxt nopre)) ))\ "Try to solve verification conditions" end