Adjust Strengthen, split out ProvePart.
This commit is contained in:
Thomas Sewell
parent
411ef475dc
commit
91ff60c978
|
|
@ -0,0 +1,182 @@
|
|||
theory ProvePart
|
||||
|
||||
imports Main
|
||||
|
||||
begin
|
||||
|
||||
text {* Introduces a (sort-of) tactic for proving part of a goal by automatic
|
||||
methods. The split between the proven and unproven part goes down into conjunction,
|
||||
implication etc. The unproven parts are left in (roughly) their original form. *}
|
||||
|
||||
text {*
|
||||
The first part is to take a goal and split it into two conjuncts,
|
||||
e.g. "a \<and> (\<forall>x. b \<and> c x)
|
||||
= (((P1 \<longrightarrow> a) \<and> (\<forall>x. (P2 \<longrightarrow> b) \<and> (P3 \<longrightarrow> c x)))
|
||||
\<and> ((\<not> P1 \<longrightarrow> a) \<and> (\<forall>x. (\<not> P2 \<longrightarrow> b) \<and> (\<not> P3 \<longrightarrow> c x)))"
|
||||
|
||||
The first conjunct is then attacked by some automatic method.
|
||||
|
||||
The final part is to eliminate any goals remaining after that
|
||||
automatic method by setting the Pi to False. The remaining Pi
|
||||
(whose goal fragments were solved) are set to True. If the
|
||||
resulting goals cannot be solved by setting to False, or if
|
||||
no Pi are actually set to true, the process fails.
|
||||
*}
|
||||
|
||||
lemma logic_to_conj_thm_workers:
|
||||
"A = (A' \<and> A'') \<Longrightarrow> B = (B' \<and> B'')
|
||||
\<Longrightarrow> (A \<and> B) = ((A' \<and> B') \<and> (A'' \<and> B''))"
|
||||
"B = (B' \<and> B'')
|
||||
\<Longrightarrow> (A \<or> B) = ((A \<or> B') \<and> (A \<or> B''))"
|
||||
"\<lbrakk> \<And>x. P x = (P' x \<and> P'' x) \<rbrakk>
|
||||
\<Longrightarrow> (\<forall>x. P x) = ((\<forall>x. P' x) \<and> (\<forall>x. P'' x))"
|
||||
"\<lbrakk> \<And>x. P x = (P' x \<and> P'' x) \<rbrakk>
|
||||
\<Longrightarrow> (\<forall>x \<in> S. P x) = ((\<forall>x \<in> S. P' x) \<and> (\<forall>x \<in> S. P'' x))"
|
||||
"B = (B' \<and> B'')
|
||||
\<Longrightarrow> (A \<longrightarrow> B) = ((A \<longrightarrow> B') \<and> (A \<longrightarrow> B''))"
|
||||
by auto
|
||||
|
||||
ML {*
|
||||
structure Split_To_Conj = struct
|
||||
|
||||
fun abs_name (Abs (s, _, _)) = s
|
||||
| abs_name _ = "x"
|
||||
|
||||
fun all_type (Const (@{const_name "All"}, T) $ _)
|
||||
= domain_type (domain_type T)
|
||||
| all_type (Const (@{const_name "Ball"}, T) $ _ $ _)
|
||||
= domain_type (domain_type (range_type T))
|
||||
| all_type t = raise TERM ("all_type", [t])
|
||||
|
||||
fun split_thm prefix ctxt t = let
|
||||
val ok = not (String.isPrefix "Q" prefix orelse String.isPrefix "R" prefix)
|
||||
val _ = ok orelse error ("split_thm: prefix has prefix Q/R: " ^ prefix)
|
||||
fun params (@{term "op \<and>"} $ x $ y) Ts = params x Ts @ params y Ts
|
||||
| params (@{term "op \<or>"} $ _ $ y) Ts = (Ts, SOME @{typ bool}) :: params y Ts
|
||||
| params (all as (Const (@{const_name "All"}, _) $ t)) Ts
|
||||
= params (betapply (t, Bound 0)) (all_type all :: Ts)
|
||||
| params (ball as (Const (@{const_name "Ball"}, T) $ _ $ t)) Ts
|
||||
= (Ts, SOME (domain_type T)) :: params (betapply (t, Bound 0)) (all_type ball :: Ts)
|
||||
| params (@{term "op \<longrightarrow>"} $ _ $ t) Ts = (Ts, SOME @{typ bool}) :: params t Ts
|
||||
| params _ Ts = [(Ts, NONE)]
|
||||
val ps = params t []
|
||||
val Ps = Variable.variant_frees ctxt [t]
|
||||
(replicate (length ps) (prefix, @{typ bool}))
|
||||
|> map Free
|
||||
val Qs = Variable.variant_frees ctxt [t]
|
||||
(map (fn (ps, T) => case T of NONE => ("Q", ps ---> @{typ bool})
|
||||
| SOME T => ("R", ps ---> T)) ps)
|
||||
|> map Free
|
||||
val Qs = map (fn (Q, (ps, _)) => Term.list_comb (Q, map Bound (0 upto (length ps - 1))))
|
||||
(Qs ~~ ps)
|
||||
fun assemble_bits (@{term "op \<and>"} $ x $ y) Ps = let
|
||||
val (x, Ps) = assemble_bits x Ps
|
||||
val (y, Ps) = assemble_bits y Ps
|
||||
in (@{term "op \<and>"} $ x $ y, Ps) end
|
||||
| assemble_bits (@{term "op \<or>"} $ _ $ y) Ps = let
|
||||
val x = hd Ps
|
||||
val (y, Ps) = assemble_bits y (tl Ps)
|
||||
in (@{term "op \<or>"} $ x $ y, Ps) end
|
||||
| assemble_bits (all as (Const (@{const_name "All"}, T) $ t)) Ps = let
|
||||
val nm = abs_name t
|
||||
val (t, Ps) = assemble_bits (betapply (t, Bound 0)) Ps
|
||||
in (Const (@{const_name "All"}, T) $ Abs (nm, all_type all, t), Ps) end
|
||||
| assemble_bits (ball as (Const (@{const_name "Ball"}, T) $ _ $ t)) Ps = let
|
||||
val nm = abs_name t
|
||||
val S = hd Ps
|
||||
val (t, Ps) = assemble_bits (betapply (t, Bound 0)) (tl Ps)
|
||||
in (Const (@{const_name "Ball"}, T) $ S $ Abs (nm, all_type ball, t), Ps) end
|
||||
| assemble_bits (@{term "op \<longrightarrow>"} $ _ $ y) Ps = let
|
||||
val x = hd Ps
|
||||
val (y, Ps) = assemble_bits y (tl Ps)
|
||||
in (@{term "op \<longrightarrow>"} $ x $ y, Ps) end
|
||||
| assemble_bits _ Ps = (hd Ps, tl Ps)
|
||||
val bits_lhs = assemble_bits t Qs |> fst
|
||||
fun imp tf (P, Q) = if String.isPrefix "R" (fst (dest_Free (head_of Q))) then Q
|
||||
else HOLogic.mk_imp (if tf then P else HOLogic.mk_not P, Q)
|
||||
val bits_true = assemble_bits t (map (imp true) (Ps ~~ Qs)) |> fst
|
||||
val bits_false = assemble_bits t (map (imp false) (Ps ~~ Qs)) |> fst
|
||||
val concl = HOLogic.mk_eq (bits_lhs, HOLogic.mk_conj (bits_true, bits_false))
|
||||
|> HOLogic.mk_Trueprop
|
||||
in (Goal.prove ctxt (map (fst o dest_Free o head_of) Qs) [] concl
|
||||
(K (REPEAT_ALL_NEW (resolve_tac ctxt
|
||||
@{thms logic_to_conj_thm_workers cases_simp[symmetric]}) 1)),
|
||||
map dest_Free Ps)
|
||||
end
|
||||
|
||||
fun get_split_tac prefix ctxt tac = SUBGOAL (fn (t, i) =>
|
||||
let
|
||||
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl t)
|
||||
val (thm, Ps) = split_thm prefix ctxt concl
|
||||
in (rtac @{thm iffD2} THEN' rtac thm THEN' tac Ps) end i)
|
||||
|
||||
end
|
||||
*}
|
||||
|
||||
text {* Testing. *}
|
||||
|
||||
ML {*
|
||||
Split_To_Conj.split_thm "P" @{context}
|
||||
@{term "x & y & (\<forall>t \<in> UNIV. \<forall>n. True \<longrightarrow> z t n)"}
|
||||
*}
|
||||
|
||||
ML {*
|
||||
structure Partial_Prove = struct
|
||||
|
||||
fun inst_frees_tac ctxt Ps ct = REPEAT_DETERM o SUBGOAL (fn (t, _) =>
|
||||
fn thm => case Term.add_frees t [] |> filter (member (op =) Ps)
|
||||
of [] => Seq.empty
|
||||
| (f :: _) => let
|
||||
val idx = Thm.maxidx_of thm + 1
|
||||
val var = Thm.cterm_of ctxt (Var ((fst f, idx), snd f))
|
||||
in thm |> Thm.generalize ([], [fst f]) idx
|
||||
|> Thm.instantiate ([], [(var, ct)])
|
||||
|> Seq.single
|
||||
end)
|
||||
|
||||
fun cleanup_tac ctxt Ps
|
||||
= inst_frees_tac ctxt Ps @{cterm False}
|
||||
THEN' asm_full_simp_tac ctxt
|
||||
|
||||
fun finish_tac ctxt Ps = inst_frees_tac ctxt Ps @{cterm True}
|
||||
THEN' CONVERSION (Conv.concl_conv ~1 (Simplifier.rewrite (put_simpset HOL_ss ctxt)))
|
||||
|
||||
fun test_start_partial_prove ctxt i t = let
|
||||
val j = Thm.nprems_of t - i
|
||||
in Split_To_Conj.get_split_tac ("P_" ^ string_of_int j ^ "_") ctxt
|
||||
(K (K all_tac)) i t
|
||||
end
|
||||
|
||||
fun test_end_partial_prove ctxt t = let
|
||||
fun match_P (s, T) = case space_explode "_" s of
|
||||
["P", n, _] => try (fn () => ((s, T), the (Int.fromString n))) ()
|
||||
| _ => NONE
|
||||
val Ps = Term.add_frees (Thm.concl_of t) [] |> map_filter match_P
|
||||
fun getmax ((x, n) :: xs) max maxes = if n > max then getmax xs n [x]
|
||||
else getmax xs max maxes
|
||||
| getmax [] max maxes = (max, maxes)
|
||||
val (j, Ps) = getmax Ps 0 []
|
||||
val i = Thm.nprems_of t - j
|
||||
in REPEAT_DETERM (FIRSTGOAL (fn k => if k < i then cleanup_tac ctxt Ps k else no_tac))
|
||||
THEN finish_tac ctxt Ps i end t
|
||||
|
||||
fun partial_prove tactic ctxt i
|
||||
= Split_To_Conj.get_split_tac ("P_" ^ string_of_int i ^ "_") ctxt
|
||||
(fn Ps => fn i => tactic i THEN finish_tac ctxt Ps i) i
|
||||
|
||||
fun method (ctxtg, []) = (fn ctxt => Method.SIMPLE_METHOD (test_start_partial_prove ctxt 1),
|
||||
(ctxtg, []))
|
||||
| method args = error "Partial_Prove: still working on that"
|
||||
|
||||
fun fin_method () = Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (test_end_partial_prove ctxt))
|
||||
|
||||
end
|
||||
*}
|
||||
|
||||
method_setup partial_prove = {* Partial_Prove.method *}
|
||||
"partially prove a compound goal by some automatic method"
|
||||
|
||||
method_setup finish_partial_prove = {* Partial_Prove.fin_method () *}
|
||||
"partially prove a compound goal by some automatic method"
|
||||
|
||||
end
|
||||
|
|
@ -6,26 +6,119 @@ begin
|
|||
|
||||
text {* Strengthen *}
|
||||
|
||||
definition
|
||||
"strengthen_imp rel x y = (x = y \<or> rel x y)"
|
||||
locale strengthen_implementation begin
|
||||
|
||||
lemma strengthen_imp_refl:
|
||||
"strengthen_imp rel x x"
|
||||
by (simp add: strengthen_imp_def)
|
||||
definition "st P rel x y = (x = y \<or> (P \<and> rel x y) \<or> (\<not> P \<and> rel y x))"
|
||||
|
||||
lemma strengthen_impI:
|
||||
"rel x y \<Longrightarrow> strengthen_imp rel x y"
|
||||
by (simp add: strengthen_imp_def)
|
||||
definition "failed == True"
|
||||
|
||||
lemmas imp_to_strengthen = strengthen_impI[where rel="op \<longrightarrow>"]
|
||||
definition elim :: "prop \<Rightarrow> prop"
|
||||
where
|
||||
"elim (P :: prop) == P"
|
||||
|
||||
definition "oblig (P :: prop) == P"
|
||||
|
||||
end
|
||||
|
||||
notation strengthen_implementation.elim ("{elim| _ |}")
|
||||
notation strengthen_implementation.oblig ("{oblig| _ |}")
|
||||
notation strengthen_implementation.failed ("<strg-failed>")
|
||||
|
||||
syntax
|
||||
"_ap_strg_bool" :: "['a, 'a] => 'a" ("_ =strg<--|=> _")
|
||||
"_ap_wkn_bool" :: "['a, 'a] => 'a" ("_ =strg-->|=> _")
|
||||
"_ap_ge_bool" :: "['a, 'a] => 'a" ("_ =strg<=|=> _")
|
||||
"_ap_le_bool" :: "['a, 'a] => 'a" ("_ =strg>=|=> _")
|
||||
|
||||
syntax(xsymbols)
|
||||
"_ap_strg_bool" :: "['a, 'a] => 'a" ("_ =strg\<longleftarrow>|=> _")
|
||||
"_ap_wkn_bool" :: "['a, 'a] => 'a" ("_ =strg\<longrightarrow>|=> _")
|
||||
"_ap_ge_bool" :: "['a, 'a] => 'a" ("_ =strg\<le>|=> _")
|
||||
"_ap_le_bool" :: "['a, 'a] => 'a" ("_ =strg\<ge>|=> _")
|
||||
|
||||
translations
|
||||
"P =strg\<longleftarrow>|=> Q" == "CONST strengthen_implementation.st (CONST False) (CONST HOL.implies) P Q"
|
||||
"P =strg\<longrightarrow>|=> Q" == "CONST strengthen_implementation.st (CONST True) (CONST HOL.implies) P Q"
|
||||
"P =strg\<le>|=> Q" == "CONST strengthen_implementation.st (CONST False) (CONST Orderings.less_eq) P Q"
|
||||
"P =strg\<ge>|=> Q" == "CONST strengthen_implementation.st (CONST True) (CONST Orderings.less_eq) P Q"
|
||||
|
||||
context strengthen_implementation begin
|
||||
|
||||
lemma failedI:
|
||||
"<strg-failed>"
|
||||
by (simp add: failed_def)
|
||||
|
||||
lemma strengthen_refl:
|
||||
"st P rel x x"
|
||||
by (simp add: st_def)
|
||||
|
||||
lemma strengthenI:
|
||||
"rel x y \<Longrightarrow> st True rel x y"
|
||||
"rel y x \<Longrightarrow> st False rel x y"
|
||||
by (simp_all add: st_def)
|
||||
|
||||
lemmas imp_to_strengthen = strengthenI(2)[where rel="op \<longrightarrow>"]
|
||||
lemmas rev_imp_to_strengthen = strengthenI(1)[where rel="op \<longrightarrow>"]
|
||||
lemmas ord_to_strengthen = strengthenI[where rel="op \<le>"]
|
||||
|
||||
lemma use_strengthen_imp:
|
||||
"strengthen_imp (op \<longrightarrow>) P Q \<Longrightarrow> P \<Longrightarrow> Q"
|
||||
by (simp add: strengthen_imp_def)
|
||||
"st False (op \<longrightarrow>) Q P \<Longrightarrow> P \<Longrightarrow> Q"
|
||||
by (simp add: st_def)
|
||||
|
||||
lemma strengthen_Not:
|
||||
"st False rel x y \<Longrightarrow> st (\<not> True) rel x y"
|
||||
"st True rel x y \<Longrightarrow> st (\<not> False) rel x y"
|
||||
by auto
|
||||
|
||||
lemmas gather =
|
||||
swap_prems_eq[where A="PROP (Trueprop P)" and B="PROP (elim Q)" for P Q]
|
||||
swap_prems_eq[where A="PROP (Trueprop P)" and B="PROP (oblig Q)" for P Q]
|
||||
|
||||
lemma mk_True_imp:
|
||||
"P \<equiv> True \<longrightarrow> P"
|
||||
by simp
|
||||
|
||||
lemma narrow_quant:
|
||||
"(\<And>x. PROP P \<Longrightarrow> PROP (Q x)) \<equiv> (PROP P \<Longrightarrow> (\<And>x. PROP (Q x)))"
|
||||
"(\<And>x. (R \<longrightarrow> S x)) \<equiv> PROP (Trueprop (R \<longrightarrow> (\<forall>x. S x)))"
|
||||
"(\<And>x. (S x \<longrightarrow> R)) \<equiv> PROP (Trueprop ((\<exists>x. S x) \<longrightarrow> R))"
|
||||
apply (simp_all add: atomize_all)
|
||||
apply rule
|
||||
apply assumption
|
||||
apply assumption
|
||||
done
|
||||
|
||||
ML {*
|
||||
structure Make_Strengthen_Rule = struct
|
||||
|
||||
fun binop_conv' cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2;
|
||||
|
||||
val mk_elim = Conv.rewr_conv @{thm elim_def[symmetric]}
|
||||
val mk_oblig = Conv.rewr_conv @{thm oblig_def[symmetric]}
|
||||
|
||||
fun count_vars t = Term.fold_aterms
|
||||
(fn (Var v) => Termtab.map_default (Var v, 0) (fn x => x + 1)
|
||||
| _ => I) t Termtab.empty
|
||||
|
||||
fun gather_to_imp ctxt drule pattern = let
|
||||
val pattern = (if drule then "D" :: pattern else pattern)
|
||||
fun inner pat ct = case (head_of (Thm.term_of ct), pat) of
|
||||
(@{term Pure.imp}, ("E" :: pat)) => binop_conv' mk_elim (inner pat) ct
|
||||
| (@{term Pure.imp}, ("O" :: pat)) => binop_conv' mk_oblig (inner pat) ct
|
||||
| (@{term Pure.imp}, _) => binop_conv' (Object_Logic.atomize ctxt) (inner (drop 1 pat)) ct
|
||||
| (_, []) => Object_Logic.atomize ctxt ct
|
||||
| (_, pat) => raise THM ("gather_to_imp: leftover pattern: " ^ commas pat, 1, [])
|
||||
fun simp thms = Raw_Simplifier.rewrite ctxt false thms
|
||||
fun ensure_imp ct = case (strip_comb (Thm.term_of ct) |> apsnd (map head_of)) of
|
||||
(@{term Pure.imp}, []) => Conv.arg_conv ensure_imp ct
|
||||
| (@{term HOL.Trueprop}, [@{term HOL.implies}]) => Conv.all_conv ct
|
||||
| _ => Conv.rewr_conv @{thm mk_True_imp} ct
|
||||
val gather = simp @{thms gather}
|
||||
then_conv (if drule then Conv.all_conv else simp @{thms atomize_conjL})
|
||||
then_conv simp @{thms atomize_imp}
|
||||
then_conv ensure_imp
|
||||
in Conv.fconv_rule (inner pattern then_conv gather) end
|
||||
|
||||
fun imp_list t = let
|
||||
val (x, y) = Logic.dest_implies t
|
||||
in x :: imp_list y end handle TERM _ => [t]
|
||||
|
|
@ -33,55 +126,74 @@ fun imp_list t = let
|
|||
fun mk_ex (xnm, T) t = HOLogic.exists_const T $ Term.lambda (Var (xnm, T)) t
|
||||
fun mk_all (xnm, T) t = HOLogic.all_const T $ Term.lambda (Var (xnm, T)) t
|
||||
|
||||
fun do_mk ctxt thm = let
|
||||
val atomize = Object_Logic.atomize_prems ctxt (Thm.cprop_of thm)
|
||||
val thm2 = Thm.equal_elim atomize thm
|
||||
val xs = imp_list (Thm.term_of (Thm.rhs_of atomize))
|
||||
val xs = map HOLogic.dest_Trueprop xs
|
||||
handle TERM _ => raise TERM ("Make_Strengthen_Rule.mk: Trueprop", xs)
|
||||
val (concl :: rev_prems) = rev xs
|
||||
val prem = fold (curry HOLogic.mk_conj) (rev rev_prems) @{term True}
|
||||
val free_concl = Term.add_vars concl []
|
||||
val free_prem = Term.add_vars prem []
|
||||
val ord = prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord
|
||||
val ex_free_prem = Ord_List.subtract ord (Ord_List.make ord free_concl)
|
||||
(Ord_List.make ord free_prem)
|
||||
val ex_prem = fold mk_ex ex_free_prem prem
|
||||
val imp = (@{term "strengthen_imp (op -->)"}
|
||||
$ ex_prem $ concl)
|
||||
val rule = @{term Trueprop} $ fold mk_all free_concl imp |> Thm.cterm_of ctxt
|
||||
in Goal.prove_internal ctxt [] rule
|
||||
(K (
|
||||
REPEAT_DETERM (rtac @{thm allI} 1)
|
||||
THEN rtac @{thm strengthen_impI} 1
|
||||
THEN rtac @{thm impI} 1
|
||||
THEN (REPEAT_DETERM (etac @{thm exE} 1))
|
||||
THEN rtac thm2 1
|
||||
THEN ALLGOALS (fn i => REPEAT_DETERM_N (length xs - i - 1) (dtac @{thm conjunct2} i))
|
||||
THEN ALLGOALS (dtac @{thm conjunct1})
|
||||
THEN ALLGOALS atac
|
||||
))
|
||||
|> Object_Logic.rulify ctxt
|
||||
fun quantify_vars ctxt drule thm = let
|
||||
val (lhs, rhs) = Thm.concl_of thm |> HOLogic.dest_Trueprop
|
||||
|> HOLogic.dest_imp
|
||||
val all_vars = count_vars (Thm.prop_of thm)
|
||||
val new_vars = count_vars (if drule then rhs else lhs)
|
||||
val quant = filter (fn v => Termtab.lookup new_vars v = Termtab.lookup all_vars v)
|
||||
(Termtab.keys new_vars)
|
||||
|> map (Thm.cterm_of ctxt)
|
||||
in fold Thm.forall_intr quant thm
|
||||
|> Conv.fconv_rule (Raw_Simplifier.rewrite ctxt false @{thms narrow_quant})
|
||||
end
|
||||
|
||||
fun mk_thm ctxt thm = (HOLogic.dest_Trueprop (Thm.prop_of thm);
|
||||
thm RS @{thm imp_to_strengthen})
|
||||
handle TERM _ => do_mk ctxt thm
|
||||
handle THM _ => raise THM ("Make_Strengthen_Rule.mk_thm:"
|
||||
^ " not impl or meta-impl", 1, [thm])
|
||||
fun mk_strg (typ, pat) ctxt thm = let
|
||||
val drule = typ = "D" orelse typ = "D'"
|
||||
val imp = gather_to_imp ctxt drule pat thm
|
||||
|> (if typ = "I'" orelse typ = "D'"
|
||||
then quantify_vars ctxt drule else I)
|
||||
in if typ = "I" orelse typ = "I'"
|
||||
then imp RS @{thm imp_to_strengthen}
|
||||
else if drule then imp RS @{thm rev_imp_to_strengthen}
|
||||
else if typ = "lhs" then imp RS @{thm ord_to_strengthen(1)}
|
||||
else if typ = "rhs" then imp RS @{thm ord_to_strengthen(2)}
|
||||
else raise THM ("mk_strg: unknown type: " ^ typ, 1, [thm])
|
||||
end
|
||||
|
||||
fun auto_mk ctxt thm = let
|
||||
val concl_C = try (fst o dest_Const o head_of
|
||||
o HOLogic.dest_Trueprop) (Thm.concl_of thm)
|
||||
in case (Thm.nprems_of thm, concl_C) of
|
||||
(_, SOME @{const_name failed}) => thm
|
||||
| (_, SOME @{const_name st}) => thm
|
||||
| (0, SOME @{const_name HOL.implies}) => (thm RS @{thm imp_to_strengthen}
|
||||
handle THM _ => @{thm failedI})
|
||||
| _ => mk_strg ("I'", []) ctxt thm
|
||||
end
|
||||
|
||||
fun mk_strg_args (SOME (typ, pat)) ctxt thm = mk_strg (typ, pat) ctxt thm
|
||||
| mk_strg_args NONE ctxt thm = auto_mk ctxt thm
|
||||
|
||||
val arg_pars = Scan.option (Scan.first (map Args.$$$ ["I", "I'", "D", "D'", "lhs", "rhs"])
|
||||
-- Scan.repeat (Args.$$$ "E" || Args.$$$ "O" || Args.$$$ "_"))
|
||||
|
||||
val setup =
|
||||
Attrib.setup @{binding "mk_strg"}
|
||||
((Scan.lift arg_pars -- Args.context)
|
||||
>> (fn (args, ctxt) => Thm.rule_attribute (K (mk_strg_args args ctxt))))
|
||||
"put rule in 'strengthen' form"
|
||||
|
||||
end
|
||||
*}
|
||||
|
||||
ML {*
|
||||
Make_Strengthen_Rule.mk_thm @{context} @{thm nat.induct}
|
||||
*}
|
||||
end
|
||||
|
||||
context strengthen_implementation begin
|
||||
|
||||
lemma do_elim:
|
||||
"PROP P \<Longrightarrow> PROP elim (PROP P)"
|
||||
by (simp add: elim_def)
|
||||
|
||||
lemma intro_oblig:
|
||||
"PROP P \<Longrightarrow> PROP oblig (PROP P)"
|
||||
by (simp add: oblig_def)
|
||||
|
||||
ML {*
|
||||
|
||||
structure Strengthen = struct
|
||||
|
||||
structure Congs = Generic_Data
|
||||
structure Congs = Theory_Data
|
||||
(struct
|
||||
type T = thm list
|
||||
val empty = []
|
||||
|
|
@ -89,38 +201,49 @@ structure Congs = Generic_Data
|
|||
val merge = Thm.merge_thms;
|
||||
end);
|
||||
|
||||
fun map_context_total f (Context.Theory t) = (Context.Theory (f t))
|
||||
| map_context_total f (Context.Proof p)
|
||||
= (Context.Proof (Context.raw_transfer (f (Proof_Context.theory_of p)) p))
|
||||
|
||||
val strg_add = Thm.declaration_attribute
|
||||
(fn thm =>
|
||||
(Congs.map (Thm.add_thm thm)));
|
||||
(fn thm => map_context_total (Congs.map (Thm.add_thm thm)));
|
||||
|
||||
val strg_del = Thm.declaration_attribute
|
||||
(fn thm =>
|
||||
(Congs.map (Thm.del_thm thm)));
|
||||
(fn thm => map_context_total (Congs.map (Thm.del_thm thm)));
|
||||
|
||||
val setup =
|
||||
Attrib.setup @{binding "strg"} (Attrib.add_del strg_add strg_del)
|
||||
"strengthening congruence rules";
|
||||
|
||||
infix 1 THEN_ALL_NEW_SOLVED;
|
||||
val do_elim = SUBGOAL (fn (t, i) => case (head_of (Logic.strip_assums_concl t)) of
|
||||
@{term elim} => etac @{thm do_elim} i
|
||||
| _ => all_tac)
|
||||
|
||||
(* Like THEN_ALL_NEW but insists at least one goal is solved
|
||||
by the various applications of tac2. *)
|
||||
fun (tac1 THEN_ALL_NEW_SOLVED tac2) i st =
|
||||
st |> (tac1 i THEN SOLVED' (fn _ => fn st' =>
|
||||
Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) st') 52);
|
||||
infix 1 THEN_TRY_ALL_NEW;
|
||||
|
||||
(* Like THEN_ALL_NEW but allows failure, although at least one subsequent
|
||||
method must succeed. *)
|
||||
fun (tac1 THEN_TRY_ALL_NEW tac2) i st = let
|
||||
fun inner b j st = if i > j then (if b then all_tac else no_tac) st
|
||||
else ((tac2 j THEN inner true (j - 1)) ORELSE inner b (j - 1)) st
|
||||
in st |> (tac1 i THEN (fn st' =>
|
||||
inner false (i + Thm.nprems_of st' - Thm.nprems_of st) st')) end
|
||||
|
||||
fun apply_strg ctxt congs rules = let
|
||||
in resolve_tac ctxt rules
|
||||
ORELSE' ((resolve_tac ctxt congs
|
||||
THEN_ALL_NEW_SOLVED (fn i => TRY (apply_strg ctxt congs rules i)))
|
||||
THEN_ALL_NEW rtac @{thm strengthen_imp_refl})
|
||||
in TRY o resolve_tac ctxt @{thms strengthen_Not}
|
||||
THEN' ((resolve_tac ctxt rules THEN_ALL_NEW do_elim)
|
||||
ORELSE' (resolve_tac ctxt congs THEN_TRY_ALL_NEW (fn i => apply_strg ctxt congs rules i)))
|
||||
end
|
||||
|
||||
fun do_strg ctxt congs rules
|
||||
= apply_strg ctxt congs rules
|
||||
THEN_ALL_NEW (TRY o resolve_tac ctxt @{thms strengthen_refl intro_oblig})
|
||||
|
||||
fun strengthen ctxt thms = let
|
||||
val congs = Congs.get (Context.Proof ctxt)
|
||||
val rules = map (Make_Strengthen_Rule.mk_thm ctxt) thms
|
||||
val congs = Congs.get (Proof_Context.theory_of ctxt)
|
||||
val rules = map (Make_Strengthen_Rule.auto_mk ctxt) thms
|
||||
in rtac @{thm use_strengthen_imp}
|
||||
THEN' apply_strg ctxt congs rules end
|
||||
THEN' do_strg ctxt congs rules end
|
||||
|
||||
val strengthen_args =
|
||||
Attrib.thms >> curry (fn (rules, ctxt) =>
|
||||
|
|
@ -133,6 +256,8 @@ end
|
|||
|
||||
*}
|
||||
|
||||
end
|
||||
|
||||
setup "Strengthen.setup"
|
||||
|
||||
method_setup strengthen = {* Strengthen.strengthen_args *}
|
||||
|
|
@ -140,142 +265,96 @@ method_setup strengthen = {* Strengthen.strengthen_args *}
|
|||
|
||||
text {* Important strengthen congruence rules. *}
|
||||
|
||||
lemma strengthen_imp_imp:
|
||||
"strengthen_imp (op \<longrightarrow>) A B = (A \<longrightarrow> B)"
|
||||
"strengthen_imp (swp (op \<longrightarrow>)) A B = (B \<longrightarrow> A)"
|
||||
by (simp_all add: strengthen_imp_def swp_def)
|
||||
context strengthen_implementation begin
|
||||
|
||||
context begin
|
||||
lemma strengthen_imp_imp[simp]:
|
||||
"st True (op \<longrightarrow>) A B = (A \<longrightarrow> B)"
|
||||
"st False (op \<longrightarrow>) A B = (B \<longrightarrow> A)"
|
||||
by (simp_all add: st_def)
|
||||
|
||||
private abbreviation(input)
|
||||
"stimp_ord a \<equiv> strengthen_imp (op \<le>) (a :: 'a :: preorder)"
|
||||
private abbreviation(input)
|
||||
"stimp_ord2 a \<equiv> strengthen_imp (swp (op \<le>)) (a :: 'a :: preorder)"
|
||||
abbreviation(input)
|
||||
"st_ord t \<equiv> st t (op \<le> :: ('a :: preorder) \<Rightarrow> _)"
|
||||
|
||||
lemma strengthen_imp_ord:
|
||||
"stimp_ord A B = (A \<le> B)"
|
||||
"stimp_ord2 A B = (B \<le> A)"
|
||||
by (auto simp add: strengthen_imp_def swp_def)
|
||||
|
||||
private declare strengthen_imp_ord[simp]
|
||||
private declare strengthen_imp_imp[simp]
|
||||
lemma strengthen_imp_ord[simp]:
|
||||
"st_ord True A B = (A \<le> B)"
|
||||
"st_ord False A B = (B \<le> A)"
|
||||
by (auto simp add: st_def)
|
||||
|
||||
lemma strengthen_imp_conj [strg]:
|
||||
"\<lbrakk> strengthen_imp (op \<longrightarrow>) A A'; strengthen_imp (op \<longrightarrow>) B B' \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (A \<and> B) (A' \<and> B')"
|
||||
by (simp add: strengthen_imp_imp)
|
||||
|
||||
lemma strengthen_imp_conj2 [strg]:
|
||||
"\<lbrakk> strengthen_imp (swp (op \<longrightarrow>)) A A'; strengthen_imp (swp (op \<longrightarrow>)) B B' \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (swp (op \<longrightarrow>)) (A \<and> B) (A' \<and> B')"
|
||||
by simp
|
||||
"\<lbrakk> B \<Longrightarrow> st F (op \<longrightarrow>) A A'; A' \<Longrightarrow> st F (op \<longrightarrow>) B B' \<rbrakk>
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (A \<and> B) (A' \<and> B')"
|
||||
by (cases F, auto)
|
||||
|
||||
lemma strengthen_imp_disj [strg]:
|
||||
"\<lbrakk> strengthen_imp (op \<longrightarrow>) A A'; strengthen_imp (op \<longrightarrow>) B B' \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (A \<or> B) (A' \<or> B')"
|
||||
by simp
|
||||
"\<lbrakk> \<not> B \<Longrightarrow> st F (op \<longrightarrow>) A A'; \<not> A' \<Longrightarrow> st F (op \<longrightarrow>) B B' \<rbrakk>
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (A \<or> B) (A' \<or> B')"
|
||||
by (cases F, auto)
|
||||
|
||||
lemma strengthen_imp_disj2 [strg]:
|
||||
"\<lbrakk> strengthen_imp (swp (op \<longrightarrow>)) A A'; strengthen_imp (swp (op \<longrightarrow>)) B B' \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (swp (op \<longrightarrow>)) (A \<or> B) (A' \<or> B')"
|
||||
by simp
|
||||
|
||||
lemma strengthen_imp [strg]:
|
||||
"\<lbrakk> strengthen_imp (swp (op \<longrightarrow>)) X X'; strengthen_imp (op \<longrightarrow>) Y Y' \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (X \<longrightarrow> Y) (X' \<longrightarrow> Y')"
|
||||
by simp
|
||||
|
||||
lemma strengthen_imp2 [strg]:
|
||||
"\<lbrakk> strengthen_imp (op \<longrightarrow>) X X'; strengthen_imp (swp (op \<longrightarrow>)) Y Y' \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (swp (op \<longrightarrow>)) (X \<longrightarrow> Y) (X' \<longrightarrow> Y')"
|
||||
by simp
|
||||
lemma strengthen_imp_implies [strg]:
|
||||
"\<lbrakk> st (\<not> F) (op \<longrightarrow>) X X'; X' \<Longrightarrow> st F (op \<longrightarrow>) Y Y' \<rbrakk>
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (X \<longrightarrow> Y) (X' \<longrightarrow> Y')"
|
||||
by (cases F, auto)
|
||||
|
||||
lemma strengthen_all[strg]:
|
||||
"\<lbrakk> \<And>x. strengthen_imp (op \<longrightarrow>) (P x) (Q x) \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (\<forall>x. P x) (\<forall>x. Q x)"
|
||||
by auto
|
||||
|
||||
lemma strengthen_all2[strg]:
|
||||
"\<lbrakk> \<And>x. strengthen_imp (swp (op \<longrightarrow>)) (P x) (Q x) \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (swp (op \<longrightarrow>)) (\<forall>x. P x) (\<forall>x. Q x)"
|
||||
by auto
|
||||
"\<lbrakk> \<And>x. st F (op \<longrightarrow>) (P x) (Q x) \<rbrakk>
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (\<forall>x. P x) (\<forall>x. Q x)"
|
||||
by (cases F, auto)
|
||||
|
||||
lemma strengthen_ex[strg]:
|
||||
"\<lbrakk> \<And>x. strengthen_imp (op \<longrightarrow>) (P x) (Q x) \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (\<exists>x. P x) (\<exists>x. Q x)"
|
||||
by auto
|
||||
|
||||
lemma strengthen_ex2[strg]:
|
||||
"\<lbrakk> \<And>x. strengthen_imp (swp (op \<longrightarrow>)) (P x) (Q x) \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (swp (op \<longrightarrow>)) (\<exists>x. P x) (\<exists>x. Q x)"
|
||||
by auto
|
||||
"\<lbrakk> \<And>x. st F (op \<longrightarrow>) (P x) (Q x) \<rbrakk>
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (\<exists>x. P x) (\<exists>x. Q x)"
|
||||
by (cases F, auto)
|
||||
|
||||
lemma strengthen_Ball[strg]:
|
||||
"\<lbrakk> \<And>x. strengthen_imp (op \<longrightarrow>) (P x) (Q x);
|
||||
stimp_ord2 S S' \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (\<forall>x \<in> S. P x) (\<forall>x \<in> S. Q x)"
|
||||
by auto
|
||||
|
||||
lemma strengthen_Ball2[strg]:
|
||||
"\<lbrakk> \<And>x. strengthen_imp (swp (op \<longrightarrow>)) (P x) (Q x);
|
||||
stimp_ord S S' \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (swp (op \<longrightarrow>)) (\<forall>x \<in> S. P x) (\<forall>x \<in> S'. Q x)"
|
||||
by auto
|
||||
"\<lbrakk> st_ord (Not F) S S';
|
||||
\<And>x. x \<in> S' \<Longrightarrow> st F (op \<longrightarrow>) (P x) (Q x) \<rbrakk>
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (\<forall>x \<in> S. P x) (\<forall>x \<in> S'. Q x)"
|
||||
by (cases F, auto)
|
||||
|
||||
lemma strengthen_Bex[strg]:
|
||||
"\<lbrakk> \<And>x. strengthen_imp (op \<longrightarrow>) (P x) (Q x);
|
||||
stimp_ord2 S S' \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (\<exists>x \<in> S. P x) (\<exists>x \<in> S. Q x)"
|
||||
by auto
|
||||
|
||||
lemma strengthen_Bex2[strg]:
|
||||
"\<lbrakk> \<And>x. strengthen_imp (swp (op \<longrightarrow>)) (P x) (Q x);
|
||||
stimp_ord S S' \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (swp (op \<longrightarrow>)) (\<exists>x \<in> S. P x) (\<exists>x \<in> S. Q x)"
|
||||
by auto
|
||||
"\<lbrakk> st_ord F S S';
|
||||
\<And>x. x \<in> S' \<Longrightarrow> st F (op \<longrightarrow>) (P x) (Q x) \<rbrakk>
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (\<exists>x \<in> S. P x) (\<exists>x \<in> S'. Q x)"
|
||||
by (cases F, auto)
|
||||
|
||||
lemma strengthen_Collect[strg]:
|
||||
"\<lbrakk> \<And>x. strengthen_imp (op \<longrightarrow>) (P x) (P' x) \<rbrakk>
|
||||
\<Longrightarrow> stimp_ord {x. P x} {x. P' x}"
|
||||
by auto
|
||||
|
||||
lemma strengthen_Collect2[strg]:
|
||||
"\<lbrakk> \<And>x. strengthen_imp (swp (op \<longrightarrow>)) (P x) (P' x) \<rbrakk>
|
||||
\<Longrightarrow> stimp_ord2 {x. P x} {x. P' x}"
|
||||
by auto
|
||||
"\<lbrakk> \<And>x. st F (op \<longrightarrow>) (P x) (P' x) \<rbrakk>
|
||||
\<Longrightarrow> st_ord F {x. P x} {x. P' x}"
|
||||
by (cases F, auto)
|
||||
|
||||
lemma strengthen_mem[strg]:
|
||||
"\<lbrakk> strengthen_imp (op \<le>) S S' \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (x \<in> S) (x \<in> S')"
|
||||
by auto
|
||||
|
||||
lemma strengthen_mem2[strg]:
|
||||
"\<lbrakk> strengthen_imp (swp (op \<le>)) S S' \<rbrakk>
|
||||
\<Longrightarrow> strengthen_imp (swp (op \<longrightarrow>)) (x \<in> S) (x \<in> S')"
|
||||
by auto
|
||||
"\<lbrakk> st_ord F S S' \<rbrakk>
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (x \<in> S) (x \<in> S')"
|
||||
by (cases F, auto)
|
||||
|
||||
lemma strengthen_ord[strg]:
|
||||
"stimp_ord2 x x' \<Longrightarrow> stimp_ord y y'
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (x \<le> y) (x' \<le> y')"
|
||||
by (simp, metis order_trans)
|
||||
|
||||
lemma strengthen_ord2[strg]:
|
||||
"stimp_ord x x' \<Longrightarrow> stimp_ord2 y y'
|
||||
\<Longrightarrow> strengthen_imp (swp (op \<longrightarrow>)) (x \<le> y) (x' \<le> y')"
|
||||
by (simp, metis order_trans)
|
||||
"st_ord (\<not> F) x x' \<Longrightarrow> st_ord F y y'
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (x \<le> y) (x' \<le> y')"
|
||||
by (cases F, simp_all, (metis order_trans)+)
|
||||
|
||||
lemma strengthen_strict_ord[strg]:
|
||||
"stimp_ord2 x x' \<Longrightarrow> stimp_ord y y'
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (x < y) (x' < y')"
|
||||
by (simp, metis order_le_less_trans order_less_le_trans)
|
||||
"st_ord (\<not> F) x x' \<Longrightarrow> st_ord F y y'
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (x < y) (x' < y')"
|
||||
by (cases F, simp_all, (metis order_le_less_trans order_less_le_trans)+)
|
||||
|
||||
lemma strengthen_strict_ord2[strg]:
|
||||
"stimp_ord x x' \<Longrightarrow> stimp_ord2 y y'
|
||||
\<Longrightarrow> strengthen_imp (swp (op \<longrightarrow>)) (x < y) (x' < y')"
|
||||
by (simp, metis order_le_less_trans order_less_le_trans)
|
||||
lemma strengthen_image[strg]:
|
||||
"st_ord F S S' \<Longrightarrow> st_ord F (f ` S) (f ` S')"
|
||||
by (cases F, auto)
|
||||
|
||||
(* FIXME: add image, revimage, restrict_map, Int, Un, all variants
|
||||
of big set UN/INT syntax, all relevant order stuff, etc. *)
|
||||
lemma strengthen_vimage[strg]:
|
||||
"st_ord F S S' \<Longrightarrow> st_ord F (f -` S) (f -` S')"
|
||||
by (cases F, auto)
|
||||
|
||||
lemma strengthen_Int[strg]:
|
||||
"st_ord F A A' \<Longrightarrow> st_ord F B B' \<Longrightarrow> st_ord F (A \<inter> B) (A' \<inter> B')"
|
||||
by (cases F, auto)
|
||||
|
||||
lemma strengthen_Un[strg]:
|
||||
"st_ord F A A' \<Longrightarrow> st_ord F B B' \<Longrightarrow> st_ord F (A \<union> B) (A' \<union> B')"
|
||||
by (cases F, auto)
|
||||
|
||||
(* FIXME: add all variants
|
||||
of big set UN/INT syntax, maps, all relevant order stuff, etc. *)
|
||||
|
||||
lemma imp_consequent:
|
||||
"P \<longrightarrow> Q \<longrightarrow> P" by simp
|
||||
|
|
|
|||
|
|
@ -2141,25 +2141,29 @@ lemma validE_NF_condition [wp]:
|
|||
|
||||
text {* Strengthen setup. *}
|
||||
|
||||
context strengthen_implementation begin
|
||||
|
||||
lemma strengthen_hoare [strg]:
|
||||
"(\<And>r s. strengthen_imp (op \<longrightarrow>) (Q r s) (R r s))
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>)"
|
||||
by (auto elim: hoare_strengthen_post)
|
||||
"(\<And>r s. st F (op \<longrightarrow>) (Q r s) (R r s))
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>)"
|
||||
by (cases F, auto elim: hoare_strengthen_post)
|
||||
|
||||
lemma strengthen_validE_R_cong[strg]:
|
||||
"(\<And>r s. strengthen_imp (op \<longrightarrow>) (Q r s) (R r s))
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -)"
|
||||
by (auto intro: hoare_post_imp_R)
|
||||
"(\<And>r s. st F (op \<longrightarrow>) (Q r s) (R r s))
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -)"
|
||||
by (cases F, auto intro: hoare_post_imp_R)
|
||||
|
||||
lemma strengthen_validE_cong[strg]:
|
||||
"(\<And>r s. strengthen_imp (op \<longrightarrow>) (Q r s) (R r s))
|
||||
\<Longrightarrow> (\<And>r s. strengthen_imp (op \<longrightarrow>) (S r s) (T r s))
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>)"
|
||||
by (auto elim: hoare_post_impErr)
|
||||
"(\<And>r s. st F (op \<longrightarrow>) (Q r s) (R r s))
|
||||
\<Longrightarrow> (\<And>r s. st F (op \<longrightarrow>) (S r s) (T r s))
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>)"
|
||||
by (cases F, auto elim: hoare_post_impErr)
|
||||
|
||||
lemma strengthen_validE_E_cong[strg]:
|
||||
"(\<And>r s. strengthen_imp (op \<longrightarrow>) (S r s) (T r s))
|
||||
\<Longrightarrow> strengthen_imp (op \<longrightarrow>) (\<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace>) (\<lbrace>P\<rbrace> f -, \<lbrace>T\<rbrace>)"
|
||||
by (auto elim: hoare_post_impErr simp: validE_E_def)
|
||||
"(\<And>r s. st F (op \<longrightarrow>) (S r s) (T r s))
|
||||
\<Longrightarrow> st F (op \<longrightarrow>) (\<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace>) (\<lbrace>P\<rbrace> f -, \<lbrace>T\<rbrace>)"
|
||||
by (cases F, auto elim: hoare_post_impErr simp: validE_E_def)
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1,120 +1,17 @@
|
|||
theory WPBang
|
||||
|
||||
imports WP "../Strengthen" NonDetMonadVCG
|
||||
imports WP "../ProvePart" NonDetMonadVCG
|
||||
|
||||
begin
|
||||
|
||||
text {*
|
||||
Splitting up predicates in a particular way.
|
||||
*}
|
||||
|
||||
lemma logic_to_conj_thm_workers:
|
||||
"A = (A' \<and> A'') \<Longrightarrow> B = (B' \<and> B'')
|
||||
\<Longrightarrow> (A \<and> B) = ((A' \<and> B') \<and> (A'' \<and> B''))"
|
||||
"B = (B' \<and> B'')
|
||||
\<Longrightarrow> (A \<or> B) = ((A \<or> B') \<and> (A \<or> B''))"
|
||||
"\<lbrakk> \<And>x. P x = (P' x \<and> P'' x) \<rbrakk>
|
||||
\<Longrightarrow> (\<forall>x. P x) = ((\<forall>x. P' x) \<and> (\<forall>x. P'' x))"
|
||||
"\<lbrakk> \<And>x. P x = (P' x \<and> P'' x) \<rbrakk>
|
||||
\<Longrightarrow> (\<forall>x \<in> S. P x) = ((\<forall>x \<in> S. P' x) \<and> (\<forall>x \<in> S. P'' x))"
|
||||
"B = (B' \<and> B'')
|
||||
\<Longrightarrow> (A \<longrightarrow> B) = ((A \<longrightarrow> B') \<and> (A \<longrightarrow> B''))"
|
||||
by auto
|
||||
|
||||
ML {*
|
||||
structure Split_To_Conj = struct
|
||||
(* Split a composite predicate into two, see test example below. *)
|
||||
|
||||
fun abs_name (Abs (s, _, _)) = s
|
||||
| abs_name _ = "x"
|
||||
|
||||
fun all_type (Const (@{const_name "All"}, T) $ _)
|
||||
= domain_type (domain_type T)
|
||||
| all_type (Const (@{const_name "Ball"}, T) $ _ $ _)
|
||||
= domain_type (domain_type (range_type T))
|
||||
| all_type t = raise TERM ("all_type", [t])
|
||||
|
||||
fun split_thm ctxt t = let
|
||||
fun params (@{term "op \<and>"} $ x $ y) Ts = params x Ts @ params y Ts
|
||||
| params (@{term "op \<or>"} $ _ $ y) Ts = (Ts, SOME @{typ bool}) :: params y Ts
|
||||
| params (all as (Const (@{const_name "All"}, _) $ t)) Ts
|
||||
= params (betapply (t, Bound 0)) (all_type all :: Ts)
|
||||
| params (ball as (Const (@{const_name "Ball"}, T) $ _ $ t)) Ts
|
||||
= (Ts, SOME (domain_type T)) :: params (betapply (t, Bound 0)) (all_type ball :: Ts)
|
||||
| params (@{term "op \<longrightarrow>"} $ _ $ t) Ts = (Ts, SOME @{typ bool}) :: params t Ts
|
||||
| params _ Ts = [(Ts, NONE)]
|
||||
val ps = params t []
|
||||
val Ps = Variable.variant_frees ctxt [t]
|
||||
(replicate (length ps) ("P", @{typ bool}))
|
||||
|> map Free
|
||||
val Qs = Variable.variant_frees ctxt [t]
|
||||
(map (fn (ps, T) => case T of NONE => ("Q", ps ---> @{typ bool})
|
||||
| SOME T => ("R", ps ---> T)) ps)
|
||||
|> map Free
|
||||
val Qs = map (fn (Q, (ps, _)) => Term.list_comb (Q, map Bound (0 upto (length ps - 1))))
|
||||
(Qs ~~ ps)
|
||||
fun assemble_bits (@{term "op \<and>"} $ x $ y) Ps = let
|
||||
val (x, Ps) = assemble_bits x Ps
|
||||
val (y, Ps) = assemble_bits y Ps
|
||||
in (@{term "op \<and>"} $ x $ y, Ps) end
|
||||
| assemble_bits (@{term "op \<or>"} $ _ $ y) Ps = let
|
||||
val x = hd Ps
|
||||
val (y, Ps) = assemble_bits y (tl Ps)
|
||||
in (@{term "op \<or>"} $ x $ y, Ps) end
|
||||
| assemble_bits (all as (Const (@{const_name "All"}, T) $ t)) Ps = let
|
||||
val nm = abs_name t
|
||||
val (t, Ps) = assemble_bits (betapply (t, Bound 0)) Ps
|
||||
in (Const (@{const_name "All"}, T) $ Abs (nm, all_type all, t), Ps) end
|
||||
| assemble_bits (ball as (Const (@{const_name "Ball"}, T) $ _ $ t)) Ps = let
|
||||
val nm = abs_name t
|
||||
val S = hd Ps
|
||||
val (t, Ps) = assemble_bits (betapply (t, Bound 0)) (tl Ps)
|
||||
in (Const (@{const_name "Ball"}, T) $ S $ Abs (nm, all_type ball, t), Ps) end
|
||||
| assemble_bits (@{term "op \<longrightarrow>"} $ _ $ y) Ps = let
|
||||
val x = hd Ps
|
||||
val (y, Ps) = assemble_bits y (tl Ps)
|
||||
in (@{term "op \<longrightarrow>"} $ x $ y, Ps) end
|
||||
| assemble_bits _ Ps = (hd Ps, tl Ps)
|
||||
val bits_lhs = assemble_bits t Qs |> fst
|
||||
fun imp tf (P, Q) = if String.isPrefix "R" (fst (dest_Free (head_of Q))) then Q
|
||||
else HOLogic.mk_imp (if tf then P else HOLogic.mk_not P, Q)
|
||||
val bits_true = assemble_bits t (map (imp true) (Ps ~~ Qs)) |> fst
|
||||
val bits_false = assemble_bits t (map (imp false) (Ps ~~ Qs)) |> fst
|
||||
val concl = HOLogic.mk_eq (bits_lhs, HOLogic.mk_conj (bits_true, bits_false))
|
||||
|> HOLogic.mk_Trueprop
|
||||
in Goal.prove ctxt (map (fst o dest_Free o head_of) Qs) [] concl
|
||||
(K (REPEAT_ALL_NEW (resolve_tac ctxt
|
||||
@{thms logic_to_conj_thm_workers cases_simp[symmetric]}) 1))
|
||||
end
|
||||
|
||||
end
|
||||
*}
|
||||
|
||||
text {* Testing the split. *}
|
||||
ML {*
|
||||
Split_To_Conj.split_thm @{context}
|
||||
@{term "x & y & (\<forall>t \<in> UNIV. \<forall>n. True \<longrightarrow> z t n)"}
|
||||
*}
|
||||
|
||||
lemma conj_prove_lhsE:
|
||||
"P \<and> Q \<Longrightarrow> (P \<Longrightarrow> P') \<Longrightarrow> P' \<and> Q"
|
||||
lemma conj_meta_forward:
|
||||
"P \<and> Q \<Longrightarrow> (P \<Longrightarrow> P') \<Longrightarrow> (Q \<Longrightarrow> Q') \<Longrightarrow> P' \<and> Q'"
|
||||
by simp
|
||||
|
||||
text {* Applying safe WP rules. *}
|
||||
ML {*
|
||||
structure WP_Safe = struct
|
||||
|
||||
fun inst_frees_tac ctxt Ps ct = REPEAT_DETERM o SUBGOAL (fn (t, _) =>
|
||||
fn thm => case Term.add_frees t [] |> filter (member (op =) Ps)
|
||||
of [] => Seq.empty
|
||||
| (f :: _) => let
|
||||
val idx = Thm.maxidx_of thm + 1
|
||||
val var = Thm.cterm_of ctxt (Var ((fst f, idx), snd f))
|
||||
in thm |> Thm.generalize ([], [fst f]) idx
|
||||
|> Thm.instantiate ([], [(var, ct)])
|
||||
|> Seq.single
|
||||
end)
|
||||
|
||||
fun check_has_frees_tac Ps (_ : int) thm = let
|
||||
val fs = Term.add_frees (Thm.prop_of thm) [] |> filter (member (op =) Ps)
|
||||
in if null fs then Seq.empty else Seq.single thm end
|
||||
|
|
@ -125,19 +22,13 @@ fun wp_bang wp_safe_rules ctxt = let
|
|||
|> map (rotate_prems 1)
|
||||
in
|
||||
resolve_tac ctxt wp_safe_rules_conj
|
||||
THEN' SUBGOAL (fn (t, i) => let
|
||||
val eq_to_conj_thm = Split_To_Conj.split_thm ctxt
|
||||
(HOLogic.dest_Trueprop (Logic.strip_assums_concl t))
|
||||
val Ps = Term.add_frees (Thm.prop_of eq_to_conj_thm) []
|
||||
in rtac @{thm iffD2} i THEN rtac eq_to_conj_thm i
|
||||
THEN etac @{thm conj_prove_lhsE} i
|
||||
THEN (REPEAT_ALL_NEW ((CHANGED o asm_full_simp_tac ctxt) ORELSE' Classical.safe_steps_tac ctxt)
|
||||
THEN_ALL_NEW inst_frees_tac ctxt Ps @{cterm "False"}
|
||||
THEN_ALL_NEW (check_has_frees_tac Ps THEN' asm_full_simp_tac ctxt)
|
||||
) i
|
||||
THEN inst_frees_tac ctxt Ps @{cterm "True"} i
|
||||
THEN simp_tac ctxt i
|
||||
end)
|
||||
THEN' Split_To_Conj.get_split_tac "P" ctxt
|
||||
(fn Ps => fn i => etac @{thm conj_meta_forward} i
|
||||
THEN (REPEAT_ALL_NEW ((CHANGED o asm_full_simp_tac ctxt)
|
||||
ORELSE' Classical.safe_steps_tac ctxt)
|
||||
THEN_ALL_NEW Partial_Prove.cleanup_tac ctxt Ps) i
|
||||
THEN (Partial_Prove.finish_tac ctxt Ps THEN' atac) i
|
||||
)
|
||||
end
|
||||
|
||||
val wpe_args =
|
||||
|
|
@ -154,7 +45,8 @@ method_setup wpe = {* WP_Safe.wpe_args *}
|
|||
"applies 'safe' wp rules to eliminate postcondition components"
|
||||
|
||||
text {* Testing. *}
|
||||
lemma
|
||||
|
||||
lemma
|
||||
assumes x: "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv. Q \<rbrace>"
|
||||
and y: "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv. R \<rbrace>"
|
||||
shows
|
||||
|
|
@ -162,6 +54,10 @@ lemma
|
|||
\<and> (snd rv = Some y \<longrightarrow> Q s )
|
||||
\<and> R s \<rbrace>"
|
||||
apply (rule hoare_pre)
|
||||
apply (simp add: all_conj_distrib)
|
||||
apply (rule hoare_vcg_conj_lift)
|
||||
apply (wpe x)
|
||||
apply wp
|
||||
apply (wpe x)
|
||||
apply (wp y)
|
||||
apply simp
|
||||
|
|
|
|||
Loading…
Reference in New Issue