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