
diff -r 3b9c05d158f3 -r a2142526bb01 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Fri Mar 26 09:23:23 2010 +0100
+++ b/Nominal/Fv.thy	Fri Mar 26 10:07:26 2010 +0100
@@ -198,11 +198,6 @@
       if a = b then a else
       HOLogic.mk_binop @{const_name sup} (a, b)) (rev sets) noatoms;
   val mk_inter = foldr1 (HOLogic.mk_binop @{const_name inf})
-  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};
   fun mk_diff a b =
     if b = noatoms then a else
     if b = a then noatoms else
@@ -597,102 +592,7 @@
 end
 *}
 
-(*
-atom_decl name
-datatype lam =
-  VAR "name"
-| APP "lam" "lam"
-| LET "bp" "lam"
-and bp =
-  BP "name" "lam"
-primrec
-  bi::"bp \<Rightarrow> atom set"
-where
-  "bi (BP x t) = {atom x}"
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *}
-local_setup {*
-  snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam")
-  [[[], [], [(SOME (@{term bi}, true), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *}
-print_theorems
-*)
 
-(*atom_decl name
-datatype rtrm1 =
-  rVr1 "name"
-| rAp1 "rtrm1" "rtrm1"
-| rLm1 "name" "rtrm1"        --"name is bound in trm1"
-| rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"
-and bp =
-  BUnit
-| BVr "name"
-| BPr "bp" "bp"
-primrec
-  bv1
-where
-  "bv1 (BUnit) = {}"
-| "bv1 (BVr x) = {atom x}"
-| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm1") 2 *}
-local_setup {*
-  snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm1")
-  [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, false), 0, 2)]],
-  [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *}
-print_theorems
-*)
-
-(*
-atom_decl name
-datatype rtrm5 =
-  rVr5 "name"
-| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
-and rlts =
-  rLnil
-| rLcons "name" "rtrm5" "rlts"
-primrec
-  rbv5
-where
-  "rbv5 rLnil = {}"
-| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.rtrm5") 2 *}
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.rtrm5")
-  [[[], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}
-print_theorems
-*)
-
-ML {*
-fun alpha_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_alpha_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_alpha_inj intrs dist_inj elims ctxt =
-let
-  val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;
-  val gls = map (HOLogic.mk_Trueprop o build_alpha_inj_gl) thms_imp;
-  fun tac _ = alpha_inj_tac dist_inj intrs elims 1;
-  val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;
-in
-  Variable.export ctxt' ctxt thms
-end
-*}
 
 ML {*
 fun build_alpha_sym_trans_gl alphas (x, y, z) =
@@ -746,8 +646,8 @@
 fun reflp_tac induct eq_iff ctxt =
   rtac induct THEN_ALL_NEW
   simp_tac ((mk_minimal_ss ctxt) addsimps eq_iff) THEN_ALL_NEW
-  split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
-  THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
+  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
        add_0_left supp_zero_perm Int_empty_left split_conv})
 *}
@@ -799,12 +699,12 @@
 
 ML {*
 fun symp_tac induct inj eqvt ctxt =
-  ind_tac induct THEN_ALL_NEW
-  simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conjs
+  rel_indtac induct THEN_ALL_NEW
+  simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conj_tac
   THEN_ALL_NEW
   REPEAT o etac @{thm exi_neg}
   THEN_ALL_NEW
-  split_conjs THEN_ALL_NEW
+  split_conj_tac THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
   TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW
   (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
@@ -864,12 +764,12 @@
 
 ML {*
 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
-  ind_tac induct THEN_ALL_NEW
+  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
-  split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conjs
+  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_conjs THEN_ALL_NEW
+  THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
   TRY o (etac @{thm alpha_gen_compose_trans2} ORELSE' etac @{thm alpha_gen_compose_trans}) THEN_ALL_NEW
   (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
 *}
@@ -955,7 +855,7 @@
 ML {*
 fun supports_tac perm =
   simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
-    REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN'
+    REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conj_tac THEN'
     asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
       swap_fresh_fresh fresh_atom swap_at_base_simps(3) swap_atom_image_fresh
       supp_fset_to_set supp_fmap_atom}))
@@ -1009,7 +909,7 @@
 *}
 
 ML {*
-fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW (
+fun fs_tac induct supports = rel_indtac induct THEN_ALL_NEW (
   rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set
     supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp})
@@ -1079,7 +979,7 @@
 
 ML {*
 fun supp_eq_tac ind fv perm eqiff ctxt =
-  ind_tac ind THEN_ALL_NEW
+  rel_indtac ind THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW
@@ -1099,32 +999,7 @@
   simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI})
 *}
 
-(* 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,...} = ((fn _ => print_tac (PolyML.makestring names')) THEN'
-    InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]
-    THEN_ALL_NEW split_conjs 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_loc
-in
-  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
-end
-*}
+
 
 ML {*
 fun build_eqvt_gl pi frees fnctn ctxt =
@@ -1151,34 +1026,6 @@
 *}
 
 ML {*
-fun prove_by_alpha_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);
-(*  val _ = tracing (PolyML.makestring gl); *)
-  fun tac {context,...} = (ind_tac ind THEN_ALL_NEW split_conjs 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_loc
-in
-  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
-end
-*}
-
-ML {*
 fun build_rsp_gl alphas fnctn ctxt =
 let
   val typ = domain_type (fastype_of fnctn);
@@ -1199,7 +1046,7 @@
 
 ML {*
 fun build_fvbv_rsps alphas ind simps fnctns ctxt =
-  prove_by_alpha_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps ctxt) fnctns ctxt
+  prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt
 *}
 
 end




