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