
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 \<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




