--- 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 \<Rightarrow> 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 \<Rightarrow> 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 "\<lambda>(x, y, z). \<lambda>(x', y', z'). R x x' \<and> R2 y y' \<and> R3 z z'"} *}
-
(* Given [R1, R2, R3] creates %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)
ML {*
fun mk_compound_alpha Rs =
@@ -259,8 +254,6 @@
end;
*}
-ML {* cterm_of @{theory} (mk_compound_alpha [@{term "R :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}, @{term "R2 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}, @{term "R3 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}]) *}
-
ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> 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: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>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: "\<exists>(pi :: perm). P pi \<Longrightarrow> \<exists>(pi :: perm). Q pi \<Longrightarrow> (\<And>(p :: perm) (pi :: perm). P p \<Longrightarrow> Q pi \<Longrightarrow> R (pi + p)) \<Longrightarrow> \<exists>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 \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> 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