theory LetElim
imports Main Data_slot
begin
ML {*
val _ = print_depth 100
*}
ML {*
val trace_elim = Attrib.setup_config_bool @{binding trace_elim} (K false)
*}
ML {* (* aux functions *)
val tracing = (fn ctxt => fn str =>
if (Config.get ctxt trace_elim) then tracing str else ())
val empty_env = (Vartab.empty, Vartab.empty)
fun match_env ctxt pat trm env =
Pattern.match (ctxt |> Proof_Context.theory_of) (pat, trm) env
fun match ctxt pat trm = match_env ctxt pat trm empty_env;
val inst = Envir.subst_term;
fun term_of_thm thm = thm |> prop_of |> HOLogic.dest_Trueprop
fun last [a] = a |
last (a::b) = last b
fun but_last [a] = [] |
but_last (a::b) = a::(but_last b)
fun foldr f [] = (fn x => x) |
foldr f (x :: xs) = (f x) o (foldr f xs)
fun concat [] = [] |
concat (x :: xs) = x @ concat xs
fun string_of_term ctxt t = t |> Syntax.pretty_term ctxt |> Pretty.str_of
fun string_of_cterm ctxt ct = ct |> term_of |> string_of_term ctxt
fun pterm ctxt t =
t |> string_of_term ctxt |> tracing ctxt
fun pcterm ctxt ct = ct |> string_of_cterm ctxt |> tracing ctxt
fun pthm ctxt thm = thm |> prop_of |> pterm ctxt
fun string_for_term ctxt t =
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
(print_mode_value ())) (Syntax.string_of_term ctxt) t
|> String.translate (fn c => if Char.isPrint c then str c else "")
|> Sledgehammer_Util.simplify_spaces
fun string_for_cterm ctxt ct = ct |> term_of |> string_for_term ctxt
fun attemp tac = fn i => fn st => (tac i st) handle exn => Seq.empty
fun try_tac tac = fn i => fn st => (tac i st) handle exn => (Seq.single st)
fun ctxt_show ctxt = ctxt |> Config.put Proof_Context.verbose true |>
Config.put Proof_Context.debug true |>
Config.put Display.show_hyps true |>
Config.put Display.show_tags true
fun swf f = (fn x => fn y => f y x)
*} (* aux end *)
ML {*
fun close_form_over vars trm =
fold Logic.all (map Free vars) trm
fun try_star f g = (try_star f (g |> f)) handle _ => g
fun bind_judgment ctxt name =
let
val thy = Proof_Context.theory_of ctxt;
val ([x], ctxt') = Proof_Context.add_fixes [(Binding.name name, NONE, NoSyn)] ctxt;
val (t as _ $ Free v) = Object_Logic.fixed_judgment thy x;
in ((v, t), ctxt') end;
fun let_trm_of ctxt mjp = let
fun is_let_trm (((Const (@{const_name "Let"}, _)) $ let_expr) $ let_rest) = true
| is_let_trm _ = false
in
ZipperSearch.all_td_lr (mjp |> Zipper.mktop)
|> Seq.filter (fn z => is_let_trm (Zipper.trm z))
|> Seq.hd |> Zipper.trm
end
fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME
| decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body)
| decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u)
| decr _ _ = raise Same.SAME
and decrh lev t = (decr lev t handle Same.SAME => t);
(* A new version of [result], copied from [obtain.ML] *)
fun eliminate_term ctxt xs tm =
let
val vs = map (dest_Free o Thm.term_of) xs;
val bads = Term.fold_aterms (fn t as Free v =>
if member (op =) vs v then insert (op aconv) t else I | _ => I) tm [];
val _ = null bads orelse
error ("Result contains obtained parameters: " ^
space_implode " " (map (Syntax.string_of_term ctxt) bads));
in tm end;
fun eliminate fix_ctxt rule xs As thm =
let
val thy = Proof_Context.theory_of fix_ctxt;
val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
error "Conclusion in obtained context must be object-logic judgment";
val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
val prems = Drule.strip_imp_prems (#prop (Thm.crep_thm thm'));
in
((Drule.implies_elim_list thm' (map Thm.assume prems)
|> Drule.implies_intr_list (map Drule.norm_hhf_cterm As)
|> Drule.forall_intr_list xs)
COMP rule)
|> Drule.implies_intr_list prems
|> singleton (Variable.export ctxt' fix_ctxt)
end;
fun obtain_export ctxt rule xs _ As =
(eliminate ctxt rule xs As, eliminate_term ctxt xs);
fun check_result ctxt thesis th =
(case Thm.prems_of th of
[prem] =>
if Thm.concl_of th aconv thesis andalso
Logic.strip_assums_concl prem aconv thesis then th
else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
| [] => error "Goal solved -- nothing guessed"
| _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
fun result tac facts ctxt =
let
val thy = Proof_Context.theory_of ctxt;
val cert = Thm.cterm_of thy;
val ([thesisN], _) = Variable.variant_fixes [Auto_Bind.thesisN] ctxt
val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt thesisN;
val rule =
(case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
| SOME th => check_result ctxt thesis (Raw_Simplifier.norm_hhf (Goal.conclude th)));
val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
val obtain_rule = Thm.forall_elim (cert (Logic.varify_global (Free thesis_var))) rule';
val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt';
val (prems, ctxt'') =
Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
(Drule.strip_imp_prems stmt) fix_ctxt;
in ((params, prems), ctxt'') end;
*}
ML {*
local
fun let_lhs ctxt vars let_rest =
case let_rest of
Const (@{const_name prod_case}, _) $ let_rest =>
let
val (exp1, rest1) = let_lhs ctxt vars let_rest
val vars = Term.add_frees exp1 vars
val (exp2, rest2) = let_lhs ctxt vars rest1
in ((Const (@{const_name Pair}, dummyT) $ exp1 $ exp2), rest2) end
| Abs (var, var_typ, rest) => let
val (vars', _) = Variable.variant_fixes ((map fst vars)@[var]) ctxt
val (_, var') = vars' |> split_last
val [(var, var_typ)] = Variable.variant_frees ctxt (map Free vars) [(var, var_typ)] in
(Free (var', var_typ), rest) end
fun sg_lhs_f ctxt (vars, eqns, let_trm) = let
val (((Const (@{const_name "Let"}, _)) $ let_expr) $ let_rest) = let_trm
val let_rest = case let_rest of
Abs ("", _, let_rest$Bound 0) => decrh 0 let_rest
| _ => let_rest
val (lhs, let_trm) = let_rest |> let_lhs ctxt vars
val lhs = lhs|> Syntax.check_term ctxt
val let_expr = let_expr |> Syntax.check_term ctxt
val eqn = HOLogic.mk_eq (lhs, let_expr) |> Syntax.check_term ctxt
val eqns = (eqn::eqns)
val vars = Term.add_frees lhs vars
val let_trm = Term.subst_bounds ((map Free vars), let_trm)
in (vars, eqns, let_trm) end
fun dest_let ctxt let_trm = let
val (vars, eqns, lrest) = try_star (sg_lhs_f ctxt) ([], [], let_trm)
in (vars, eqns, lrest) end
in
fun let_elim_rule ctxt mjp = let
val ctxt = ctxt |> Variable.set_body false
val thy = Proof_Context.theory_of ctxt
val cterm = cterm_of thy
val tracing = tracing ctxt
val pthm = pthm ctxt
val pterm = pterm ctxt
val pcterm = pcterm ctxt
val let_trm = let_trm_of ctxt mjp
val ([pname], _) = Variable.variant_fixes ["P"] ctxt
val P = Free (pname, dummyT)
val mjp = (Const (@{const_name Trueprop}, dummyT)$(P$let_trm))
|> Syntax.check_term ctxt
val (Const (@{const_name Trueprop}, _)$((P as Free(_, _))$let_trm)) = mjp
val (vars, eqns, lrest) = dest_let ctxt let_trm
val ([thesisN], _) = Variable.variant_fixes ["let_thesis"] ctxt
val thesis_p = Free (thesisN, @{typ bool}) |> HOLogic.mk_Trueprop
val next_p = (P $ lrest) |> (HOLogic.mk_Trueprop)
val that_prems = (P $ lrest) :: (rev eqns) |> map (HOLogic.mk_Trueprop)
val that_prop = Logic.list_implies (that_prems, thesis_p)
val that_prop = close_form_over vars that_prop
fun exists_on_lhs eq = let
val (lhs, rhs) = eq |> HOLogic.dest_eq
fun exists_on vars trm = let
fun sg_exists_on (n, ty) trm = HOLogic.mk_exists (n, ty, trm)
in fold sg_exists_on vars trm end
in exists_on (Term.add_frees lhs []) eq end
fun prove_eqn ctxt0 eqn = let
val (lhs, let_expr) = eqn |> HOLogic.dest_eq
val eq_e_prop = exists_on_lhs eqn |> HOLogic.mk_Trueprop
fun case_rule_of ctxt let_expr = let
val case_rule = Induct.find_casesT ctxt (let_expr |> type_of) |> hd
val case_var = case_rule |> swf Thm.cprem_of 1 |> Thm.term_of
|> Induct.vars_of |> hd |> cterm
val mt = Thm.match (case_var, let_expr |> cterm)
val case_rule = Thm.instantiate mt case_rule
in case_rule end
val case_rule = SOME (case_rule_of ctxt0 let_expr) handle _ => NONE
val my_case_tac = case case_rule of
SOME case_rule => (rtac case_rule 1)
| _ => all_tac
val eq_e = Goal.prove ctxt0 [] [] eq_e_prop
(K (my_case_tac THEN (auto_tac ctxt0)))
in eq_e end
val peqns = eqns |> map (prove_eqn ctxt)
fun add_result thm (facts, ctxt) = let
val ((_, [fact]), ctxt1) = (result (K (REPEAT (etac @{thm exE} 1))) [thm] ctxt)
in (fact::facts, ctxt1) end
val add_results = fold add_result
val (facts, ctxt1) = add_results (rev peqns) ([], ctxt)
(* val facts = rev facts *)
val ([mjp_p, that_p], ctxt2) = ctxt1 |> Assumption.add_assumes (map cterm [mjp, that_prop])
val sym_facts = map (swf (curry (op RS)) @{thm sym}) facts
fun rsn eq that_p = eq RSN (2, that_p)
val rule1 = fold rsn (rev facts) that_p
val tac = (Method.insert_tac ([mjp_p]@sym_facts) 1) THEN (auto_tac ctxt2)
val next_pp = Goal.prove ctxt [] [] next_p (K tac)
val result = next_pp RS rule1
val ctxt3 = fold (fn var => fn ctxt => (Variable.auto_fixes var ctxt))
[mjp, thesis_p] ctxt2
val [let_elim_rule] = Proof_Context.export ctxt3 ctxt [result]
in let_elim_rule end
fun let_intro_rule ctxt mjp = let
val ctxt = ctxt |> Variable.set_body false
val thy = Proof_Context.theory_of ctxt
val cterm = cterm_of thy
val tracing = tracing ctxt
val pthm = pthm ctxt
val pterm = pterm ctxt
val pcterm = pcterm ctxt
val ([thesisN], _) = Variable.variant_fixes ["let_thesis"] ctxt
val thesis_p = Free (thesisN, @{typ bool}) |> HOLogic.mk_Trueprop
val let_trm = let_trm_of ctxt mjp
val ([pname], _) = Variable.variant_fixes ["P"] ctxt
val P = Free (pname, dummyT)
val mjp = (Const (@{const_name Trueprop}, dummyT)$(P$let_trm))
|> Syntax.check_term ctxt
val (Const (@{const_name Trueprop}, _)$((P as Free(_, _))$let_trm)) = mjp
val (((Const (@{const_name "Let"}, _)) $ let_expr) $ let_rest) = let_trm
val (vars, eqns, lrest) = dest_let ctxt let_trm
val next_p = (P $ lrest) |> (HOLogic.mk_Trueprop)
val that_prems = (rev eqns) |> map (HOLogic.mk_Trueprop)
val that_prop = Logic.list_implies (that_prems, next_p)
val that_prop = close_form_over vars that_prop |> Syntax.check_term ctxt
fun exists_on_lhs eq = let
val (lhs, rhs) = eq |> HOLogic.dest_eq
fun exists_on vars trm = let
fun sg_exists_on (n, ty) trm = HOLogic.mk_exists (n, ty, trm)
in fold sg_exists_on vars trm end
in exists_on (Term.add_frees lhs []) eq end
fun prove_eqn ctxt0 eqn = let
val (lhs, let_expr) = eqn |> HOLogic.dest_eq
val eq_e_prop = exists_on_lhs eqn |> HOLogic.mk_Trueprop
fun case_rule_of ctxt let_expr = let
val case_rule = Induct.find_casesT ctxt (let_expr |> type_of) |> hd
val case_var = case_rule |> swf Thm.cprem_of 1 |> Thm.term_of
|> Induct.vars_of |> hd |> cterm
val mt = Thm.match (case_var, let_expr |> cterm)
val case_rule = Thm.instantiate mt case_rule
in case_rule end
val case_rule = SOME (case_rule_of ctxt0 let_expr) handle _ => NONE
val my_case_tac = case case_rule of
SOME case_rule => (rtac case_rule 1)
| _ => all_tac
val eq_e = Goal.prove ctxt0 [] [] eq_e_prop
(K (my_case_tac THEN (auto_tac ctxt0)))
in eq_e end
val peqns = eqns |> map (prove_eqn ctxt)
fun add_result thm (facts, ctxt) = let
val ((_, [fact]), ctxt1) = (result (K (REPEAT (etac @{thm exE} 1))) [thm] ctxt)
in (fact::facts, ctxt1) end
val add_results = fold add_result
val (facts, ctxt1) = add_results (rev peqns) ([], ctxt)
val sym_facts = map (swf (curry (op RS)) @{thm sym}) facts
val ([that_p], ctxt2) = ctxt1 |> Assumption.add_assumes (map cterm [that_prop])
fun rsn eq that_p = eq RSN (1, that_p)
val rule1 = fold rsn (rev facts) that_p
val tac = (Method.insert_tac (rule1::sym_facts) 1) THEN (auto_tac ctxt2)
val result = Goal.prove ctxt [] [] mjp (K tac)
val ctxt3 = fold (fn var => fn ctxt => (Variable.auto_fixes var ctxt))
[mjp, thesis_p] ctxt2
val [let_intro_rule] = Proof_Context.export ctxt3 ctxt [result]
in let_intro_rule end
end
*}
ML {*
fun let_elim_tac ctxt i st = let
val thy = Proof_Context.theory_of ctxt
val cterm = cterm_of thy
val goal = nth (Thm.prems_of st) (i - 1) |> cterm
val mjp = goal |> Drule.strip_imp_prems |> swf nth 0 |> term_of
val rule = let_elim_rule ctxt mjp
val tac = (etac rule i st)
in tac end
*}
ML {*
local
val case_names_tagN = "case_names";
val implode_args = space_implode ";";
val explode_args = space_explode ";";
fun add_case_names NONE = I
| add_case_names (SOME names) =
Thm.untag_rule case_names_tagN
#> Thm.tag_rule (case_names_tagN, implode_args names);
in
fun let_elim_cases_tac ctxt facts = let
val tracing = tracing ctxt
val pthm = pthm ctxt
val pterm = pterm ctxt
val pcterm = pcterm ctxt
val mjp = facts |> swf nth 0 |> prop_of
val _ = tracing "let_elim_cases_tac: elim rule derived is:"
val rule = (let_elim_rule ctxt mjp) |> Rule_Cases.put_consumes (SOME 1)
|> add_case_names (SOME ["LetE"])
val _ = rule |> pthm
in
Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts
end
end
*}
ML {*
val ctxt = @{context}
val thy = Proof_Context.theory_of ctxt
val cterm = cterm_of thy
val mjp = @{prop "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3
in f w x1 y1 u)"}
*}
ML {*
val mjp1 = @{prop "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = e2 in (w +x1 *y1 +u))"}
val mjp2 = @{prop "P (let ((x, y), (z, u)) = e; (u, v) = e1 in
(case u of (Some t) \<Rightarrow> f t x y z |
None \<Rightarrow> g x y z))"}
val mjp3 = @{prop "P (let x = e1; ((x1, y1), u) = e2 in f x w x1 y1 u)"}
val mjp = @{prop "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3
in f w x1 y1 u)"}
val mjps = [mjp1, mjp2, mjp3, mjp]
val t = mjps |> map (let_elim_rule ctxt)
val t2 = mjps |> map (let_intro_rule ctxt)
*}
ML {*
val let_elim_setup =
Method.setup @{binding let_elim}
(Scan.lift (Args.mode Induct.no_simpN) >>
(fn no_simp => fn ctxt =>
METHOD_CASES (fn facts => (HEADGOAL
(let_elim_cases_tac ctxt facts)))))
"elimination of prems containing lets ";
*}
setup {* let_elim_setup *}
ML {*
val ctxt = @{context}
val mjp = @{prop "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3 x1
in f w x1 y1 u)"}
*}
ML {*
fun focus_params t ctxt =
let
val (xs, Ts) =
split_list (Term.variant_frees t (Term.strip_all_vars t)); (*as they are printed :-*)
(* val (xs', ctxt') = variant_fixes xs ctxt; *)
(* val ps = xs' ~~ Ts; *)
val ps = xs ~~ Ts
val (_, ctxt'') = ctxt |> Variable.add_fixes xs
in ((xs, ps), ctxt'') end
fun focus_concl ctxt t =
let
val ((xs, ps), ctxt') = focus_params t ctxt
val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t);
in (t' |> Logic.strip_imp_concl, ctxt') end
*}
ML {*
local
val case_names_tagN = "case_names";
val implode_args = space_implode ";";
val explode_args = space_explode ";";
fun add_case_names NONE = I
| add_case_names (SOME names) =
Thm.untag_rule case_names_tagN
#> Thm.tag_rule (case_names_tagN, implode_args names);
in
fun let_intro_cases_tac ctxt facts i st = let
val (mjp, _) = nth (Thm.prems_of st) (i - 1) |> focus_concl ctxt
val rule = (let_intro_rule ctxt mjp) |> add_case_names (SOME ["LetI"])
in
Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts i st
end
end
*}
ML {*
val let_intro_setup =
Method.setup @{binding let_intro}
(Scan.lift (Args.mode Induct.no_simpN) >>
(fn no_simp => fn ctxt =>
METHOD_CASES (fn facts => (HEADGOAL
(let_intro_cases_tac ctxt facts)))))
"introduction rule for goals containing lets ";
*}
setup {* let_intro_setup *}
lemma assumes "Q xxx" "W uuuu"
shows "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3 x1
in f w x1 y1 u) = www"
using assms
proof(let_intro)
case (LetI x y w ww x1 y1 u x2 y2)
thus ?case
oops
lemma
assumes "P (let (((x, y), w), ww) = e1; ((x1, y1), u) = g x y w; (x2, y2) = e3 x1
in f w x1 y1 u)"
and "Q xxx" "W uuuu"
shows "thesis" using assms
proof(let_elim)
case (LetE x y w ww x1 y1 u x2 y2)
thus ?case
oops
ML {*
val mjp = @{prop "P ( case (u@v) of
Nil \<Rightarrow> f u v
| x#xs \<Rightarrow> g u v x xs
)"}
val mjp1 = @{term "( case (h u v) of
None \<Rightarrow> g u v x
| Some x \<Rightarrow> (case v of
Nil \<Rightarrow> f u v |
x#xs \<Rightarrow> h x xs
)
)"}
*}
ML {*
fun case_trm_of ctxt mjp =
ZipperSearch.all_td_lr (mjp |> Zipper.mktop)
|> Seq.filter (fn z => ((Case_Translation.strip_case ctxt true (Zipper.trm z)) <> NONE))
|> Seq.hd |> Zipper.trm
*}
ML {*
fun case_elim_rule ctxt mjp = let
val ctxt = ctxt |> Variable.set_body false
val thy = Proof_Context.theory_of ctxt;
val cterm = cterm_of thy
val ([thesisN], _) = Variable.variant_fixes ["my_thesis"] ctxt
val ((_, thesis_p), _) = bind_judgment ctxt thesisN
val case_trm = case_trm_of ctxt mjp
val (case_expr, case_eqns) = case_trm |> Case_Translation.strip_case ctxt true |> the
val ([pname], _) = Variable.variant_fixes ["P"] ctxt
val P = Free (pname, [(case_trm |> type_of)] ---> @{typ bool})
val mjp_p = (P $ case_trm) |> HOLogic.mk_Trueprop
val ctxt0 = Proof_Context.init_global thy
val thats = case_eqns |> map (fn (lhs, rhs) => let
val vars = Term.add_frees lhs []
in
Logic.list_implies ([(P$rhs)|>HOLogic.mk_Trueprop,
HOLogic.mk_eq (case_expr, lhs) |> HOLogic.mk_Trueprop], thesis_p) |>
close_form_over vars
end) |>
map (Term.map_types (Term.map_type_tvar (fn _ => dummyT))) |>
map (Syntax.check_term ctxt0)
val (mjp_p::that_ps, ctxt1) = ctxt |> Assumption.add_assumes (map cterm (mjp_p::thats))
fun case_rule_of ctxt let_expr = let
val case_rule = Induct.find_casesT ctxt (let_expr |> type_of) |> hd
val case_var = case_rule |> swf Thm.cprem_of 1 |> Thm.term_of
|> Induct.vars_of |> hd |> cterm
val mt = Thm.match (case_var, let_expr |> cterm)
val case_rule = Thm.instantiate mt case_rule
in case_rule end
val case_rule = case_rule_of ctxt case_expr
val my_case_tac = (rtac case_rule)
val my_tac = ((Method.insert_tac (mjp_p::that_ps)) THEN' my_case_tac THEN' (K (auto_tac ctxt1))) 1
val result = Goal.prove ctxt1 [] [] thesis_p (K my_tac)
val ctxt2 = fold (fn var => fn ctxt => (Variable.auto_fixes var ctxt))
[P, thesis_p, mjp] ctxt1
val [case_elim_rule] = Proof_Context.export ctxt2 ctxt [result]
val ocase_rule = Induct.find_casesT ctxt (case_expr |> type_of) |> hd
fun get_case_names rule =
AList.lookup (op =) (Thm.get_tags rule) "case_names" |> the
fun put_case_names names rule =
Thm.tag_rule ("case_names", names) rule
val case_elim_rule = put_case_names (get_case_names ocase_rule) case_elim_rule
in case_elim_rule end
*}
ML {*
fun case_elim_cases_tac ctxt facts = let
val mjp = facts |> swf nth 0 |> prop_of
val rule = (case_elim_rule ctxt mjp) |> Rule_Cases.put_consumes (SOME 1)
in
Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts
end
*}
ML {*
val case_elim_setup =
Method.setup @{binding case_elim}
(Scan.lift (Args.mode Induct.no_simpN) >>
(fn no_simp => fn ctxt =>
METHOD_CASES (fn facts => (HEADGOAL
(case_elim_cases_tac ctxt facts)))))
"elimination of prems containing case ";
*}
setup {* case_elim_setup *}
lemma assumes
"P (case h u v of None \<Rightarrow> g u v x | Some x \<Rightarrow> case v of [] \<Rightarrow> f u v | x # xs \<Rightarrow> h x xs)"
"GG u v" "PP w x"
shows "thesis" using assms
proof(case_elim) (* ccc *)
case None
thus ?case oops
(*
next
case (Some x)
thus ?case
proof(case_elim)
case Nil
thus ?case sorry
next
case (Cons y ys)
thus ?case sorry
qed
qed
*)
ML {*
fun case_intro_rule ctxt mjp = let
val ctxt = ctxt |> Variable.set_body false
val tracing = tracing ctxt
val pthm = pthm ctxt
val pterm = pterm ctxt
val pcterm = pcterm ctxt
val thy = Proof_Context.theory_of ctxt
val cterm = cterm_of thy
val ([thesisN], _) = Variable.variant_fixes ["my_thesis"] ctxt
val ((_, thesis_p), _) = bind_judgment ctxt thesisN
val case_trm = case_trm_of ctxt mjp
val (case_expr, case_eqns) = case_trm |> Case_Translation.strip_case ctxt true |> the
val ([pname], _) = Variable.variant_fixes ["P"] ctxt
val P = Free (pname, [(case_trm |> type_of)] ---> @{typ bool})
val mjp_p = (P $ case_trm) |> HOLogic.mk_Trueprop
val ctxt0 = Proof_Context.init_global thy
val thats = case_eqns |> map (fn (lhs, rhs) => let
val vars = Term.add_frees lhs []
in
Logic.list_implies ([HOLogic.mk_eq (case_expr, lhs) |> HOLogic.mk_Trueprop],
(P$rhs)|>HOLogic.mk_Trueprop) |>
close_form_over vars
end) |>
map (Term.map_types (Term.map_type_tvar (fn _ => dummyT))) |>
map (Syntax.check_term ctxt0)
val (that_ps, ctxt1) = ctxt |> Assumption.add_assumes (map cterm (thats))
fun case_rule_of ctxt let_expr = let
val case_rule = Induct.find_casesT ctxt (let_expr |> type_of) |> hd
val case_var = case_rule |> swf Thm.cprem_of 1 |> Thm.term_of
|> Induct.vars_of |> hd |> cterm
val mt = Thm.match (case_var, let_expr |> cterm)
val case_rule = Thm.instantiate mt case_rule
in case_rule end
val case_rule = case_rule_of ctxt case_expr
val my_case_tac = (rtac case_rule)
val my_tac = ((Method.insert_tac (that_ps)) THEN' my_case_tac THEN' (K (auto_tac ctxt1))) 1
val result = Goal.prove ctxt1 [] [] mjp_p (K my_tac)
val ctxt2 = fold (fn var => fn ctxt => (Variable.auto_fixes var ctxt))
[P, thesis_p, mjp] ctxt1
val [case_intro_rule] = Proof_Context.export ctxt2 ctxt [result]
val ocase_rule = Induct.find_casesT ctxt (case_expr |> type_of) |> hd
fun get_case_names rule =
AList.lookup (op =) (Thm.get_tags rule) "case_names" |> the
fun put_case_names names rule =
Thm.tag_rule ("case_names", names) rule
val case_intro_rule = put_case_names (get_case_names ocase_rule) case_intro_rule
in case_intro_rule end
*}
ML {*
val t = [mjp, mjp1] |> map (case_intro_rule ctxt)
*}
ML {*
fun case_intro_cases_tac ctxt facts i st = let
val (mjp, _) = nth (Thm.prems_of st) (i - 1) |> focus_concl ctxt
val rule = (case_intro_rule ctxt mjp)
in
Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts i st
end
*}
ML {*
val case_intro_setup =
Method.setup @{binding case_intro}
(Scan.lift (Args.mode Induct.no_simpN) >>
(fn no_simp => fn ctxt =>
METHOD_CASES (fn facts => (HEADGOAL
(case_intro_cases_tac ctxt facts)))))
"introduction rule for goals containing case";
*}
setup {* case_intro_setup *}
lemma assumes "QQ (let u = e1; (j, k) = e1; (b, a) = qq j k in TT j k b a)"
shows "P (hhh y ys)" using assms
proof(let_elim)
oops
lemma assumes
"QQ (let (j, k) = e1; (m, n) = qq j k in TT j k m n)"
"PP w x"
shows "P (case h u v of None \<Rightarrow> g u v x | Some x1 \<Rightarrow> case v of [] \<Rightarrow> f u v | xx # xs \<Rightarrow> hhh xx xs)"
using assms
proof(case_intro)
case None
from None(2)
show ?case
proof(let_elim)
case (LetE j k a b)
with None
show ?case oops
(*
sorry
qed
next
case (Some x1)
thus ?case
proof(case_intro)
case Nil
from Nil(3)
show ?case
proof(let_elim)
case (LetE j k a b)
with Nil show ?case sorry
qed
next
case (Cons y ys)
from Cons(3)
show ?case
proof (let_elim)
case (LetE j k u v)
with Cons
show ?case sorry
qed
qed
qed
*)
lemma assumes
"QQ (let (j, k) = e1; (m, n) = qq j k in TT j k m n)"
"PP w uux"
shows "P (case h u v of None \<Rightarrow> g u v x | Some x1 \<Rightarrow> case v of [] \<Rightarrow> f u v | xx # xs \<Rightarrow> hhh xx xs)"
using assms
proof(let_elim)
case (LetE j k m n)
thus ?case
proof(case_intro)
case None
thus ?case oops (*
next
case (Some x)
thus ?case
proof(case_intro)
case Nil
thus ?case sorry
next
case (Cons y ys)
thus ?case sorry
qed
qed
qed
*)
lemma ifE [consumes 1, case_names If_true If_false]:
assumes "P (if b then e1 else e2)"
"\<lbrakk>b; P e1\<rbrakk> \<Longrightarrow> thesis"
"\<lbrakk>\<not> b; P e2\<rbrakk> \<Longrightarrow> thesis"
shows "thesis" using assms
by (auto split:if_splits)
lemma ifI [case_names If_true If_false]:
assumes "b \<Longrightarrow> P e1" "\<not> b \<Longrightarrow> P e2"
shows "P (if b then e1 else e2)" using assms
by auto
ML {*
fun if_elim_cases_tac ctxt facts = let
val rule = @{thm ifE}
in
Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts
end
*}
ML {*
val if_elim_setup =
Method.setup @{binding if_elim}
(Scan.lift (Args.mode Induct.no_simpN) >>
(fn no_simp => fn ctxt =>
METHOD_CASES (fn facts => (HEADGOAL
(if_elim_cases_tac ctxt facts)))))
"elimination of prems containing if ";
*}
setup {* if_elim_setup *}
ML {*
fun if_intro_cases_tac ctxt facts i st = let
val rule = @{thm ifI}
in
Induct.induct_tac ctxt true [] [] [] (SOME [rule]) facts i st
end
*}
ML {*
val if_intro_setup =
Method.setup @{binding if_intro}
(Scan.lift (Args.mode Induct.no_simpN) >>
(fn no_simp => fn ctxt =>
METHOD_CASES (fn facts => (HEADGOAL
(if_intro_cases_tac ctxt facts)))))
"introduction rule for goals containing if";
*}
setup {* if_intro_setup *}
lemma assumes "(if (B x y) then f x y else g y x) = (t, p)"
"P1 xxx" "P2 yyy"
shows "that" using assms
proof(if_elim)
case If_true
thus ?case oops
(*
next
case If_false
thus ?case oops
*)
lemma assumes "P1 xx" "P2 yy"
shows "P (if b then e1 else e2)" using assms
proof(if_intro)
case If_true
thus ?case oops
(*
next
case If_false
thus ?case sorry
qed
*)
end