File ‹generalise_state.ML›
signature SPLIT_STATE =
sig val isState: Proof.context -> term -> bool
val abs_state: Proof.context -> term -> term option
val abs_var: Proof.context -> term -> (string * typ)
val split_state: Proof.context -> string -> typ -> term -> (term * term list)
val ex_tac: Proof.context -> term list -> int -> tactic
end;
signature GENERALISE =
sig
val GENERALISE: Proof.context -> int -> tactic
end
functor Generalise (structure SplitState: SPLIT_STATE) : GENERALISE =
struct
val genConj = @{thm generaliseConj};
val genImp = @{thm generaliseImp};
val genImpl = @{thm generaliseImpl};
val genAll = @{thm generaliseAll};
val gen_all = @{thm generalise_all};
val genEx = @{thm generaliseEx};
val genRefl = @{thm generaliseRefl};
val genRefl' = @{thm generaliseRefl'};
val genTrans = @{thm generaliseTrans};
val genAllShift = @{thm generaliseAllShift};
val gen_allShift = @{thm generalise_allShift};
val meta_spec = @{thm meta_spec};
val protectRefl = @{thm protectRefl};
val protectImp = @{thm protectImp};
fun gen_thm decomp (t,ct) =
let
val (ts,cts,recomb) = decomp (t,ct)
in recomb (map (gen_thm decomp) (ts~~cts)) end;
fun dest_prop (Const (@{const_name Pure.prop}, _) $ P) = P
| dest_prop t = raise TERM ("dest_prop", [t]);
fun prem_of thm = #1 (Logic.dest_implies (dest_prop (Thm.prop_of thm)));
fun conc_of thm = #2 (Logic.dest_implies (dest_prop (Thm.prop_of thm)));
fun dest_All (Const (@{const_name "All"},_)$t) = t
| dest_All t = raise TERM ("dest_All",[t]);
fun SIMPLE_OF ctxt rule prems =
let
val mx = fold (fn thm => fn i => Int.max (Thm.maxidx_of thm,i)) prems 0;
in DistinctTreeProver.discharge ctxt prems (Thm.incr_indexes (mx + 1) rule) end;
infix 0 OF_RAW
fun tha OF_RAW thb = thb COMP (Drule.incr_indexes thb tha);
fun SIMPLE_OF_RAW ctxt tha thb = SIMPLE_OF ctxt tha [thb];
datatype qantifier = Meta_all | Hol_all | Hol_ex
fun list_exists (vs, x) =
fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P)) vs x;
fun spec' cv thm =
let
val (ct1,ct2) = thm |> Thm.cprop_of |> Thm.dest_comb |> #2
|> Thm.dest_comb |> #2 |> Thm.dest_comb;
in
(case Thm.term_of ct1 of
Const (@{const_name "Trueprop"},_)
=> let
val (Var (sP,_)$Var (sV,sVT)) = HOLogic.dest_Trueprop (Thm.concl_of spec);
val cvT = Thm.ctyp_of_cterm cv;
val vT = Thm.typ_of cvT;
in Thm.instantiate
(TVars.make [(dest_TVar sVT, cvT)],
Vars.make [((sP, vT --> HOLogic.boolT), #2 (Thm.dest_comb ct2)),
((sV, vT), cv)])
spec
end
| Const (@{const_name Pure.all},_)
=> let
val (Var (sP,_)$Var (sV,sVT)) = Thm.concl_of meta_spec;
val cvT = Thm.ctyp_of_cterm cv;
val vT = Thm.typ_of cvT;
in Thm.instantiate
(TVars.make [(dest_TVar sVT, cvT)],
Vars.make [((sP, vT --> propT), ct2),
((sV, vT),cv)])
meta_spec
end
| _ => raise THM ("spec'",0,[thm]))
end;
fun split_thm qnt ctxt s T t =
let
val (t',vars) = SplitState.split_state ctxt s T t;
val vs = map (SplitState.abs_var ctxt) vars;
val prop = (case qnt of
Meta_all => Logic.list_all (vs,t')
| Hol_all => HOLogic.mk_Trueprop (HOLogic.list_all (vs, t'))
| Hol_ex => Logic.mk_implies
(HOLogic.mk_Trueprop (list_exists (vs, t')),
HOLogic.mk_Trueprop (HOLogic.mk_exists (s,T,t))))
in (case qnt of
Hol_ex => Goal.prove ctxt [] [] prop (fn _ => SplitState.ex_tac ctxt vars 1)
| _ => let
val rP = conc_of genRefl';
val thm0 = Thm.instantiate (TVars.empty, Vars.make [(dest_Var rP, Thm.cterm_of ctxt prop)]) genRefl';
fun elim_all v thm =
let
val cv = Thm.cterm_of ctxt v;
val spc = Goal.protect 0 (spec' cv thm);
in SIMPLE_OF ctxt genTrans [thm,spc] end;
val thm = fold elim_all vars thm0;
in thm end)
end;
fun eta_expand ctxt ct =
let
val mi = Thm.maxidx_of_cterm ct;
val T = domain_type (Thm.typ_of_cterm ct);
val x = Thm.cterm_of ctxt (Var (("s",mi+1),T));
in Thm.lambda x (Thm.apply ct x) end;
fun split_abs ctxt ct =
(case Thm.term_of ct of
Abs x => (x, Thm.dest_abs_global ct)
| _ => split_abs ctxt (eta_expand ctxt ct))
fun decomp ctxt (Const (@{const_name HOL.conj}, _) $ t $ t', ct) =
([t,t'],snd (Drule.strip_comb ct), fn [thm,thm'] => SIMPLE_OF ctxt genConj [thm,thm'])
| decomp ctxt ((allc as Const (@{const_name "All"},aT)) $ f, ct) =
let
val cf = snd (Thm.dest_comb ct);
val (abst as (x,T,_),(cx',cb)) = split_abs ctxt cf;
val Free (x',_) = Thm.term_of cx';
val (Const (@{const_name Pure.all},_)$Abs (s,_,_)) = genAll |> Thm.prems_of |> hd |> dest_prop;
val genAll' = Drule.rename_bvars [(s,x)] genAll;
val (Const (@{const_name Pure.all},_)$Abs (s',_,_)) = genAllShift |> Thm.prems_of |> hd |> dest_prop;
val genAllShift' = Drule.rename_bvars [(s',x)] genAllShift;
in if SplitState.isState ctxt (allc$Abs abst)
then ([Thm.term_of cb],[cb], fn [thm] =>
let val P = HOLogic.dest_Trueprop (dest_prop (prem_of thm));
val thm' = split_thm Hol_all ctxt x' T P;
val thm1 = genAllShift' OF_RAW
Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm'));
val thm2 = genAll' OF_RAW
Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm));
in SIMPLE_OF ctxt genTrans [thm1,thm2]
end)
else ([Thm.term_of cb],[cb], fn [thm] =>
genAll' OF_RAW Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm)))
end
| decomp ctxt ((exc as Const (@{const_name "Ex"},_)) $ f, ct) =
let
val cf = snd (Thm.dest_comb ct);
val (abst as (x,T,_),(cx',cb)) = split_abs ctxt cf;
val Free (x',_) = Thm.term_of cx';
val (Const (@{const_name Pure.all},_)$Abs (s,_,_)) = genEx |> Thm.prems_of |> hd |> dest_prop;
val genEx' = Drule.rename_bvars [(s,x)] genEx;
in if SplitState.isState ctxt (exc$Abs abst)
then ([Thm.term_of cb],[cb], fn [thm] =>
let val P = HOLogic.dest_Trueprop (dest_prop (prem_of thm));
val thm' = split_thm Hol_ex ctxt x' T P;
in SIMPLE_OF_RAW ctxt protectImp (Goal.protect 0 thm') end )
else ([Thm.term_of cb],[cb], fn [thm] =>
genEx' OF_RAW Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm)))
end
| decomp ctxt (Const (@{const_name HOL.implies},_)$P$Q, ct) =
let
val [cP,cQ] = (snd (Drule.strip_comb ct));
in ([Q],[cQ],fn [thm] =>
let
val X = genImp |> Thm.concl_of |> dest_prop |> Logic.dest_implies |> #1
|> dest_prop |> HOLogic.dest_Trueprop |> HOLogic.dest_imp |> #1
|> dest_Var;
val genImp' = Thm.instantiate (TVars.empty, Vars.make [(X,cP)]) genImp;
in SIMPLE_OF ctxt genImp' [thm] end)
end
| decomp ctxt (Const (@{const_name Pure.imp},_)$P$Q, ct) =
let
val [cP,cQ] = (snd (Drule.strip_comb ct));
in ([Q],[cQ],fn [thm] =>
let
val X = genImpl |> Thm.concl_of |> dest_prop |> Logic.dest_implies |> #1
|> dest_prop |> Logic.dest_implies |> #1
|> dest_Var;
val genImpl' = Thm.instantiate (TVars.empty, Vars.make [(X,cP)]) genImpl;
in SIMPLE_OF ctxt genImpl' [thm] end)
end
| decomp ctxt ((allc as Const (@{const_name Pure.all},_)) $ f, ct) =
let
val cf = snd (Thm.dest_comb ct);
val (abst as (x,T,_),(cx',cb)) = split_abs ctxt cf;
val Free (x',_) = Thm.term_of cx';
val (Const (@{const_name Pure.all},_)$Abs (s,_,_)) = gen_all |> Thm.prems_of |> hd |> dest_prop;
val gen_all' = Drule.rename_bvars [(s,x)] gen_all;
val (Const (@{const_name Pure.all},_)$Abs (s',_,_)) = gen_allShift |> Thm.prems_of |> hd |> dest_prop;
val gen_allShift' = Drule.rename_bvars [(s',x)] gen_allShift;
in if SplitState.isState ctxt (allc$Abs abst)
then ([Thm.term_of cb],[cb], fn [thm] =>
let val P = dest_prop (prem_of thm);
val thm' = split_thm Meta_all ctxt x' T P;
val thm1 = gen_allShift' OF_RAW
Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm'));
val thm2 = gen_all' OF_RAW
Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm));
in SIMPLE_OF ctxt genTrans [thm1,thm2]
end)
else ([Thm.term_of cb],[cb], fn [thm] =>
gen_all' OF_RAW Goal.protect 0 (Thm.forall_intr cx' (Goal.conclude thm)))
end
| decomp ctxt (Const (@{const_name "Trueprop"},_)$P, ct) = ([P],snd (Drule.strip_comb ct),fn [thm] => thm)
| decomp ctxt (t, ct) = ([],[], fn [] =>
let val rP = HOLogic.dest_Trueprop (dest_prop (conc_of genRefl));
in Thm.instantiate (TVars.empty, Vars.make [(dest_Var rP, ct)]) genRefl end)
fun generalise ctxt ct = gen_thm (decomp ctxt) (Thm.term_of ct,ct);
fun init ct = Thm.instantiate' [] [SOME ct] protectRefl;
fun generalise_over_tac ctxt P = SUBGOAL (fn (t, i) => fn st =>
(case P t of
SOME t' =>
let
val ct = Thm.cterm_of ctxt t';
val meta_spec_protect' = infer_instantiate ctxt [(("x", 0), ct)] @{thm meta_spec_protect};
in
(init (Thm.adjust_maxidx_cterm 0 (List.nth (Drule.cprems_of st, i - 1)))
|> resolve_tac ctxt [meta_spec_protect'] 1
|> Seq.maps (fn st' =>
Thm.bicompose NONE {flatten = true, match = false, incremented = false}
(false, Goal.conclude st', Thm.nprems_of st') i st))
end
| NONE => no_tac st))
fun generalise_over_all_states_tac ctxt i =
REPEAT (generalise_over_tac ctxt (SplitState.abs_state ctxt) i);
fun generalise_tac ctxt = CSUBGOAL (fn (ct, i) => fn st =>
let
val ct' = Thm.dest_equals_rhs (Thm.cprop_of (Thm.eta_conversion ct));
val r = Goal.conclude (generalise ctxt ct');
in (init (Thm.adjust_maxidx_cterm 0 (List.nth (Drule.cprems_of st, i - 1)))
|> (resolve_tac ctxt [r] 1 THEN resolve_tac ctxt [Drule.protectI] 1)
|> Seq.maps (fn st' =>
Thm.bicompose NONE {flatten = true, match = false, incremented = false}
(false, Goal.conclude st', Thm.nprems_of st') i st))
end)
fun GENERALISE ctxt i =
generalise_over_all_states_tac ctxt i THEN
generalise_tac ctxt i
end;