recursive function theories / UF_rec still need coding of tapes and programs
theory LetElimimports Main Data_slotbeginML {* 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) endin 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 endend*}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 {*localval 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 endend*}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'') endfun 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 {*localval 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 endend*}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 oopslemma 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 oopsML {* 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_rulein 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 assmsproof(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 qedqed*)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_rulein 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 assmsproof(let_elim) oopslemma 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 assmsproof(case_intro) case None from None(2) show ?case proof(let_elim) case (LetE j k a b) with None show ?case oops(* sorry qednext 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 qedqed*)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 assmsproof(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 qedqed*)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 autoML {* 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 assmsproof(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 assmsproof(if_intro) case If_true thus ?case oops(*next case If_false thus ?case sorryqed*)end