theory Tacsimports Mainbegin(* General not-nominal/quotient functionality useful for proving *)(* A version of case_rule_tac that takes more exhaust rules *)ML {*fun case_rules_tac ctxt0 s rules i st =let val (_, ctxt) = Variable.focus_subgoal i st ctxt0; val ty = fastype_of (ProofContext.read_term_schematic ctxt s) fun exhaust_ty thm = fastype_of (hd (Induct.vars_of (Thm.term_of (Thm.cprem_of thm 1)))); val ty_rules = filter (fn x => exhaust_ty x = ty) rules;in InductTacs.case_rule_tac ctxt0 s (hd ty_rules) i stend*}ML {*fun mk_conjl props = fold (fn a => fn b => if a = @{term True} then b else if b = @{term True} then a else HOLogic.mk_conj (a, b)) (rev props) @{term True};*}ML {*val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)*}(* Given function for buildng a goal for an input, prepares a one common goals for all the inputs and proves it by induction together *)ML {*fun prove_by_induct tys build_goal ind utac inputs ctxt =let val names = Datatype_Prop.make_tnames tys; val (names', ctxt') = Variable.variant_fixes names ctxt; val frees = map Free (names' ~~ tys); val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt'; val gls = flat gls_lists; fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls; val trm_gl_lists = map trm_gls_map frees; val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists val trm_gls = map mk_conjl trm_gl_lists; val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls); fun tac {context,...} = ( InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind] THEN_ALL_NEW split_conj_tac THEN_ALL_NEW utac) 1 val th_loc = Goal.prove ctxt'' [] [] gl tac val ths_loc = HOLogic.conj_elims th_loc val ths = Variable.export ctxt'' ctxt ths_locin filter (fn x => not (prop_of x = prop_of @{thm TrueI})) thsend*}(* An induction for a single relation is "R x y \<Longrightarrow> P x y" but for multiple relations is "(R1 x y \<longrightarrow> P x y) \<and> (R2 a b \<longrightarrow> P2 a b)" *)ML {*fun rel_indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct*}ML {*fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt =let val tys = map (domain_type o fastype_of) alphas; val names = Datatype_Prop.make_tnames tys; val (namesl, ctxt') = Variable.variant_fixes names ctxt; val (namesr, ctxt'') = Variable.variant_fixes names ctxt'; val freesl = map Free (namesl ~~ tys); val freesr = map Free (namesr ~~ tys); val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) inputs ctxt''; val gls = flat gls_lists; fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls; val trm_gl_lists = map trm_gls_map freesl; val trm_gls = map mk_conjl trm_gl_lists; val pgls = map (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr)) val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls); fun tac {context,...} = (rel_indtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW TRY o rtac @{thm TrueI} THEN_ALL_NEW utac context) 1 val th_loc = Goal.prove ctxt'' [] [] gl tac val ths_loc = HOLogic.conj_elims th_loc val ths = Variable.export ctxt'' ctxt ths_locin filter (fn x => not (prop_of x = prop_of @{thm TrueI})) thsend*}(* Code for transforming an inductive relation to a function *)ML {*fun rel_inj_tac dist_inj intrs elims = SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE' (rtac @{thm iffI} THEN' RANGE [ (eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj) ), asm_full_simp_tac (HOL_ss addsimps intrs)])*}ML {*fun build_rel_inj_gl thm = let val prop = prop_of thm; val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); fun list_conj l = foldr1 HOLogic.mk_conj l; in if hyps = [] then concl else HOLogic.mk_eq (concl, list_conj hyps) end;*}ML {*fun build_rel_inj intrs dist_inj elims ctxt =let val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt; val gls = map (HOLogic.mk_Trueprop o build_rel_inj_gl) thms_imp; fun tac _ = rel_inj_tac dist_inj intrs elims 1; val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;in Variable.export ctxt' ctxt thmsend*}ML {*fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm*}(* Introduces an implication and immediately eliminates it by cases *)ML {*fun imp_elim_tac case_rules = Subgoal.FOCUS (fn {concl, context, ...} => case term_of concl of _ $ (_ $ asm $ _) => let fun filter_fn case_rule = ( case Logic.strip_assums_hyp (prop_of case_rule) of ((_ $ asmc) :: _) => let val thy = ProofContext.theory_of context in Pattern.matches thy (asmc, asm) end | _ => false) val matching_rules = filter filter_fn case_rules in (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1 end | _ => no_tac)*}ML {*fun is_ex (Const ("Ex", _) $ Abs _) = true | is_ex _ = false;*}ML {*fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free" | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic" | dtyp_no_of_typ dts (Type (tname, Ts)) = case try (find_index (curry op = tname o fst)) dts of NONE => error "dtyp_no_of_typ: Illegal recursion" | SOME i => i*}end