diff -r 6c722e960f2e -r 38cef5407d82 thys/LetElim.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/LetElim.thy	Fri Mar 21 15:07:59 2014 +0000
@@ -0,0 +1,804 @@
+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
\ No newline at end of file