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