# HG changeset patch # User Cezary Kaliszyk # Date 1269616839 -3600 # Node ID c9d3dda79fe38c35ab7cf527941bb21c88fd9504 # Parent 9cec4269b7f979aa2702643ed7d797118179fd34 Removed remaining cheats + some cleaning. diff -r 9cec4269b7f9 -r c9d3dda79fe3 Nominal/ExCoreHaskell.thy --- a/Nominal/ExCoreHaskell.thy Fri Mar 26 10:55:13 2010 +0100 +++ b/Nominal/ExCoreHaskell.thy Fri Mar 26 16:20:39 2010 +0100 @@ -5,7 +5,7 @@ (* core haskell *) ML {* val _ = recursive := false *} -ML {* val _ = cheat_const_rsp := true *} + atom_decl var atom_decl tvar diff -r 9cec4269b7f9 -r c9d3dda79fe3 Nominal/ExPS3.thy --- a/Nominal/ExPS3.thy Fri Mar 26 10:55:13 2010 +0100 +++ b/Nominal/ExPS3.thy Fri Mar 26 16:20:39 2010 +0100 @@ -11,17 +11,17 @@ VarP "name" | AppP "exp" "exp" | LamP x::"name" e::"exp" bind x in e -| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1 +| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1 and pat3 = PVar "name" | PUnit | PPair "pat3" "pat3" binder - bp'' :: "pat3 \ atom set" + bp :: "pat3 \ atom set" where - "bp'' (PVar x) = {atom x}" -| "bp'' (PUnit) = {}" -| "bp'' (PPair p1 p2) = bp'' p1 \ bp'' p2" + "bp (PVar x) = {atom x}" +| "bp (PUnit) = {}" +| "bp (PPair p1 p2) = bp p1 \ bp p2" thm exp_pat3.fv thm exp_pat3.eq_iff @@ -30,7 +30,7 @@ thm exp_pat3.induct thm exp_pat3.distinct thm exp_pat3.fv -thm exp_pat3.supp (* The bindings are too complicated *) +thm exp_pat3.supp end diff -r 9cec4269b7f9 -r c9d3dda79fe3 Nominal/ExPS6.thy --- a/Nominal/ExPS6.thy Fri Mar 26 10:55:13 2010 +0100 +++ b/Nominal/ExPS6.thy Fri Mar 26 16:20:39 2010 +0100 @@ -8,7 +8,6 @@ (* The binding structure is too complicated, so equivalence the way we define it is not true *) -ML {* val _ = cheat_equivp := true *} ML {* val _ = recursive := false *} nominal_datatype exp6 = diff -r 9cec4269b7f9 -r c9d3dda79fe3 Nominal/Fv.thy --- a/Nominal/Fv.thy Fri Mar 26 10:55:13 2010 +0100 +++ b/Nominal/Fv.thy Fri Mar 26 16:20:39 2010 +0100 @@ -144,13 +144,9 @@ fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t | is_atom_fset thy _ = false; - -val fset_to_set = @{term "fset_to_set :: atom fset \ atom set"} *} - - (* Like map2, only if the second list is empty passes empty lists insted of error *) ML {* fun map2i _ [] [] = [] @@ -215,6 +211,7 @@ val ty = fastype_of t; val atom_ty = dest_fsetT ty --> @{typ atom}; val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; + val fset_to_set = @{term "fset_to_set :: atom fset \ atom set"} in fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)) end; @@ -241,8 +238,6 @@ end; *} -ML {* @{term "\(x, y, z). \(x', y', z'). R x x' \ R2 y y' \ R3 z z'"} *} - (* Given [R1, R2, R3] creates %(x,x'). %(y,y'). %(z,z'). R x x' \ R y y' \ R z z' *) ML {* fun mk_compound_alpha Rs = @@ -259,8 +254,6 @@ end; *} -ML {* cterm_of @{theory} (mk_compound_alpha [@{term "R :: 'a \ 'a \ bool"}, @{term "R2 :: 'b \ 'b \ bool"}, @{term "R3 :: 'b \ 'b \ bool"}]) *} - ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \ perm \ perm"}) $ p1 $ p2 *} ML {* @@ -645,7 +638,7 @@ ML {* fun reflp_tac induct eq_iff ctxt = rtac induct THEN_ALL_NEW - simp_tac ((mk_minimal_ss ctxt) addsimps eq_iff) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv @@ -662,36 +655,6 @@ end *} -ML {* -fun build_alpha_alphabn fv_alphas_lst inducts eq_iff ctxt = -let - val (fvs_alphas, ls) = split_list fv_alphas_lst; - val (_, alpha_ts) = split_list fvs_alphas; - val tys = map (domain_type o fastype_of) alpha_ts; - val names = Datatype_Prop.make_tnames tys; - val names2 = Name.variant_list names names; - val args = map Free (names ~~ tys); - val args2 = map Free (names2 ~~ tys); - fun alpha_alphabn ((alpha, (arg, arg2)), (no, l)) = - if l = [] then [] else - let - val alpha_bns = map snd l; - val lhs = alpha $ arg $ arg2; - val rhs = foldr1 HOLogic.mk_conj (map (fn x => x $ arg $ arg2) alpha_bns); - val gl = Logic.mk_implies (HOLogic.mk_Trueprop lhs, HOLogic.mk_Trueprop rhs); - fun tac _ = (etac (nth inducts no) THEN_ALL_NEW TRY o rtac @{thm TrueI} - THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps eq_iff)) 1 - val th = Goal.prove ctxt (names @ names2) [] gl tac; - in - Project_Rule.projects ctxt (1 upto length l) th - end; - val eqs = map alpha_alphabn ((alpha_ts ~~ (args ~~ args2)) ~~ ((0 upto (length ls - 1)) ~~ ls)); -in - flat eqs -end -*} - - lemma exi_neg: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (- p)) \ \pi. Q pi" apply (erule exE) apply (rule_tac x="-pi" in exI) @@ -700,7 +663,7 @@ ML {* fun symp_tac induct inj eqvt ctxt = rel_indtac induct THEN_ALL_NEW - simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conj_tac + simp_tac (HOL_basic_ss addsimps inj) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW REPEAT o etac @{thm exi_neg} THEN_ALL_NEW @@ -710,55 +673,25 @@ (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) *} -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 - ) -*} - lemma exi_sum: "\(pi :: perm). P pi \ \(pi :: perm). Q pi \ (\(p :: perm) (pi :: perm). P p \ Q pi \ R (pi + p)) \ \pi. R pi" apply (erule exE)+ apply (rule_tac x="pia + pi" in exI) by auto -ML {* -fun is_ex (Const ("Ex", _) $ Abs _) = true - | is_ex _ = false; -*} ML {* -fun eetac rule = Subgoal.FOCUS_PARAMS - (fn (focus) => - let - val concl = #concl focus - val prems = Logic.strip_imp_prems (term_of concl) - val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems - val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs - val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs - in - (etac rule THEN' RANGE[ - atac, - eresolve_tac thins - ]) 1 - end +fun eetac rule = + Subgoal.FOCUS_PARAMS (fn focus => + let + val concl = #concl focus + val prems = Logic.strip_imp_prems (term_of concl) + val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems + val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs + val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs + in + (etac rule THEN' RANGE[atac, eresolve_tac thins]) 1 + end ) *} @@ -766,7 +699,7 @@ fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = rel_indtac induct THEN_ALL_NEW (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW - asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW + asm_full_simp_tac (HOL_basic_ss addsimps alpha_inj) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW @@ -815,40 +748,6 @@ end *} -(* -Tests: -prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} -by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *}) - -prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} -by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *}) - -prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *} -by (tactic {* transp_tac @{context} @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *}) - -lemma alpha1_equivp: - "equivp alpha_rtrm1" - "equivp alpha_bp" -apply (tactic {* - (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) - THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' - resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux}) - THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' - resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux} - THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux}) -) -1 *}) -done*) - -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 -*} - lemma not_in_union: "c \ a \ b \ (c \ a \ c \ b)" by auto @@ -1025,28 +924,4 @@ end *} -ML {* -fun build_rsp_gl alphas fnctn ctxt = -let - val typ = domain_type (fastype_of fnctn); - val (argl, argr) = the (AList.lookup (op=) alphas typ); -in - ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt) end -*} - -ML {* -fun fvbv_rsp_tac' simps ctxt = - asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW - REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW - TRY o blast_tac (claset_of ctxt) -*} - -ML {* -fun build_fvbv_rsps alphas ind simps fnctns ctxt = - prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt -*} - -end diff -r 9cec4269b7f9 -r c9d3dda79fe3 Nominal/Lift.thy --- a/Nominal/Lift.thy Fri Mar 26 10:55:13 2010 +0100 +++ b/Nominal/Lift.thy Fri Mar 26 16:20:39 2010 +0100 @@ -3,6 +3,18 @@ begin ML {* +fun define_quotient_type args tac ctxt = +let + val mthd = Method.SIMPLE_METHOD tac + val mthdt = Method.Basic (fn _ => mthd) + val bymt = Proof.global_terminal_proof (mthdt, NONE) +in + bymt (Quotient_Type.quotient_type args ctxt) +end +*} + +(* Renames schematic variables in a theorem *) +ML {* fun rename_vars fnctn thm = let val vars = Term.add_vars (prop_of thm) [] diff -r 9cec4269b7f9 -r c9d3dda79fe3 Nominal/Manual/LamEx.thy --- a/Nominal/Manual/LamEx.thy Fri Mar 26 10:55:13 2010 +0100 +++ b/Nominal/Manual/LamEx.thy Fri Mar 26 16:20:39 2010 +0100 @@ -95,8 +95,8 @@ \ rLam a t \a rLam b s" lemma a3_inverse: - assumes "rLam a t \ rLam b s" - shows "\pi. (rfv t - {atom a} = rfv s - {atom b} \ (rfv t - {atom a})\* pi \ (pi \ t) \ s)" + assumes "rLam a t \a rLam b s" + shows "\pi. (rfv t - {atom a} = rfv s - {atom b} \ (rfv t - {atom a})\* pi \ (pi \ t) \a s)" using assms apply(erule_tac alpha.cases) apply(auto) @@ -104,7 +104,7 @@ text {* should be automatic with new version of eqvt-machinery *} lemma alpha_eqvt: - shows "t \ s \ (pi \ t) \ (pi \ s)" + shows "t \a s \ (pi \ t) \a (pi \ s)" apply(induct rule: alpha.induct) apply(simp add: a1) apply(simp add: a2) @@ -126,7 +126,7 @@ done lemma alpha_refl: - shows "t \ t" + shows "t \a t" apply(induct t rule: rlam.induct) apply(simp add: a1) apply(simp add: a2) @@ -136,7 +136,7 @@ done lemma alpha_sym: - shows "t \ s \ s \ t" + shows "t \a s \ s \a t" apply(induct rule: alpha.induct) apply(simp add: a1) apply(simp add: a2) @@ -152,7 +152,7 @@ done lemma alpha_trans: - shows "t1 \ t2 \ t2 \ t3 \ t1 \ t3" + shows "t1 \a t2 \ t2 \a t3 \ t1 \a t3" apply(induct arbitrary: t3 rule: alpha.induct) apply(erule alpha.cases) apply(simp_all) @@ -188,22 +188,22 @@ done lemma alpha_rfv: - shows "t \ s \ rfv t = rfv s" + shows "t \a s \ rfv t = rfv s" apply(induct rule: alpha.induct) apply(simp_all) done inductive - alpha2 :: "rlam \ rlam \ bool" ("_ \2 _" [100, 100] 100) + alpha2 :: "rlam \ rlam \ bool" ("_ \a2 _" [100, 100] 100) where - a21: "a = b \ (rVar a) \2 (rVar b)" -| a22: "\t1 \2 t2; s1 \2 s2\ \ rApp t1 s1 \2 rApp t2 s2" -| a23: "(a = b \ t \2 s) \ (a \ b \ ((a \ b) \ t) \2 s \ atom b \ rfv t)\ rLam a t \2 rLam b s" + a21: "a = b \ (rVar a) \a2 (rVar b)" +| a22: "\t1 \a2 t2; s1 \a2 s2\ \ rApp t1 s1 \a2 rApp t2 s2" +| a23: "(a = b \ t \a2 s) \ (a \ b \ ((a \ b) \ t) \a2 s \ atom b \ rfv t)\ rLam a t \a2 rLam b s" lemma fv_vars: fixes a::name assumes a1: "\x \ rfv t - {atom a}. pi \ x = x" - shows "(pi \ t) \2 ((a \ (pi \ a)) \ t)" + shows "(pi \ t) \a2 ((a \ (pi \ a)) \ t)" using a1 apply(induct t) apply(auto) @@ -222,8 +222,8 @@ lemma - assumes a1: "t \2 s" - shows "t \ s" + assumes a1: "t \a2 s" + shows "t \a s" using a1 apply(induct) apply(rule alpha.intros) @@ -254,8 +254,8 @@ sorry lemma - assumes a1: "t \ s" - shows "t \2 s" + assumes a1: "t \a s" + shows "t \a2 s" using a1 apply(induct) apply(rule alpha2.intros) @@ -445,12 +445,12 @@ done lemma rlam_distinct: - shows "\(rVar nam \ rApp rlam1' rlam2')" - and "\(rApp rlam1' rlam2' \ rVar nam)" - and "\(rVar nam \ rLam nam' rlam')" - and "\(rLam nam' rlam' \ rVar nam)" - and "\(rApp rlam1 rlam2 \ rLam nam' rlam')" - and "\(rLam nam' rlam' \ rApp rlam1 rlam2)" + shows "\(rVar nam \a rApp rlam1' rlam2')" + and "\(rApp rlam1' rlam2' \a rVar nam)" + and "\(rVar nam \a rLam nam' rlam')" + and "\(rLam nam' rlam' \a rVar nam)" + and "\(rApp rlam1 rlam2 \a rLam nam' rlam')" + and "\(rLam nam' rlam' \a rApp rlam1 rlam2)" apply auto apply (erule alpha.cases) apply (simp_all only: rlam.distinct) diff -r 9cec4269b7f9 -r c9d3dda79fe3 Nominal/Parser.thy --- a/Nominal/Parser.thy Fri Mar 26 10:55:13 2010 +0100 +++ b/Nominal/Parser.thy Fri Mar 26 16:20:39 2010 +0100 @@ -386,15 +386,16 @@ val fv_rsp = flat (map snd fv_rsp_pre); val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; + val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11; + val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] + (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11 +(* val _ = map tracing (map PolyML.makestring alpha_bn_rsps);*) fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy - else let val alpha_alphabn = build_alpha_alphabn fv_alpha_all alpha_inducts alpha_eq_iff lthy11 + else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end - val (const_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] - const_rsp_tac) raw_consts lthy11 - val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11a; - val (alpha_bn_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] - (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11a + val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] + const_rsp_tac) raw_consts lthy11a val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; diff -r 9cec4269b7f9 -r c9d3dda79fe3 Nominal/ROOT.ML --- a/Nominal/ROOT.ML Fri Mar 26 10:55:13 2010 +0100 +++ b/Nominal/ROOT.ML Fri Mar 26 16:20:39 2010 +0100 @@ -15,8 +15,9 @@ "ExLetRec", "ExTySch", "ExLeroy", + "ExPS3", + "ExPS7", + "ExCoreHaskell", "Test" -(* "ExCoreHaskell", *) -(* "ExPS3", *) (* "ExPS6", *) ]; diff -r 9cec4269b7f9 -r c9d3dda79fe3 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Fri Mar 26 10:55:13 2010 +0100 +++ b/Nominal/Rsp.thy Fri Mar 26 16:20:39 2010 +0100 @@ -3,17 +3,6 @@ begin ML {* -fun define_quotient_type args tac ctxt = -let - val mthd = Method.SIMPLE_METHOD tac - val mthdt = Method.Basic (fn _ => mthd) - val bymt = Proof.global_terminal_proof (mthdt, NONE) -in - bymt (Quotient_Type.quotient_type args ctxt) -end -*} - -ML {* fun const_rsp lthy const = let val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy) @@ -50,10 +39,6 @@ *} ML {* -fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm -*} - -ML {* fun prove_const_rsp bind consts tac ctxt = let val rsp_goals = map (const_rsp ctxt) consts @@ -120,16 +105,9 @@ ML {* -fun mk_minimal_ss ctxt = - Simplifier.context ctxt empty_ss - setsubgoaler asm_simp_tac - setmksimps (mksimps []) -*} - -ML {* fun alpha_eqvt_tac induct simps ctxt = rel_indtac induct THEN_ALL_NEW - simp_tac ((mk_minimal_ss ctxt) addsimps simps) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps @@ -153,8 +131,6 @@ end *} -ML {* fold_map build_alpha_eqvt *} - ML {* fun build_alpha_eqvts funs tac ctxt = let @@ -256,4 +232,44 @@ end *} +ML {* +fun build_alpha_alpha_bn_gl alphas alpha_bn ctxt = +let + val ty = domain_type (fastype_of alpha_bn); + val (l, r) = the (AList.lookup (op=) alphas ty); +in + ([alpha_bn $ l $ r], ctxt) end +*} + +ML {* +fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt = + prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind + (fn _ => asm_full_simp_tac (HOL_ss addsimps simps)) alpha_bns ctxt +*} + +ML {* +fun build_rsp_gl alphas fnctn ctxt = +let + val typ = domain_type (fastype_of fnctn); + val (argl, argr) = the (AList.lookup (op=) alphas typ); +in + ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt) +end +*} + +ML {* +fun fvbv_rsp_tac' simps ctxt = + asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW + REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW + TRY o blast_tac (claset_of ctxt) +*} + +ML {* +fun build_fvbv_rsps alphas ind simps fnctns ctxt = + prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt +*} + +end diff -r 9cec4269b7f9 -r c9d3dda79fe3 Nominal/Tacs.thy --- a/Nominal/Tacs.thy Fri Mar 26 10:55:13 2010 +0100 +++ b/Nominal/Tacs.thy Fri Mar 26 16:20:39 2010 +0100 @@ -125,5 +125,46 @@ end *} +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