# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268749667 -3600
# Node ID 7c8cd6eae8e2c789b1ad46d3cbb2c962f816c641
# Parent  49bdb8d475df5727fa3e62dc136aaf9c444a0208
FV_bn generated for recursive functions as well, and used in main fv for bindings.

diff -r 49bdb8d475df -r 7c8cd6eae8e2 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue Mar 16 12:08:37 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 16 15:27:47 2010 +0100
@@ -154,6 +154,16 @@
 end
 *}
 
+ML {*
+fun all_binds l =
+let
+  fun is_non_rec (SOME (f, _), _, _) = SOME f
+    | is_non_rec _ = NONE
+in
+  distinct (op =) (map_filter is_non_rec (flat (flat l)))
+end
+*}
+
 (* We assume no bindings in the type on which bn is defined *)
 ML {*
 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) =
@@ -244,8 +254,6 @@
   length (distinct (op =) (map (fn ((b, _, _), _) => b) l)) = 1
 *}
 
-ML {* fn x => split_list(flat x) *}
-ML {* fn x => apsnd flat (split_list (map split_list x)) *}
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
 ML {*
 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy =
@@ -257,8 +265,9 @@
     "fv_" ^ name_of_typ (nth_dtyp i)) descr);
   val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
+  val all_bns = all_binds bindsall;
   val nr_bns = non_rec_binds bindsall;
-  val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;
+  val rel_bns = filter (fn (bn, _, _) => bn mem all_bns) bns;
   val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns);
   val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
   val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
@@ -297,13 +306,21 @@
             @{term "{} :: atom set"}
         | fv_bind args (SOME (f, _), i, _) = f $ (nth args i);
       fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
-      fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE
-        | find_nonrec_binder _ _ = NONE
+      fun find_compound_binder j (SOME (f, r), i, _) = if i = j then SOME (f, r) else NONE
+        | find_compound_binder _ _ = NONE
       fun fv_arg ((dt, x), arg_no) =
-        case get_first (find_nonrec_binder arg_no) bindcs of
-          SOME f =>
+        case get_first (find_compound_binder arg_no) bindcs of
+          SOME (f, is_rec) =>
             (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of
-                SOME fv_bn => fv_bn $ x
+                SOME fv_bn =>
+                  if is_rec then
+                    let
+                      val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs;
+                      val sub = fv_binds args relevant
+                    in
+                      mk_diff (fv_bn $ x) sub
+                    end
+                  else fv_bn $ x
               | NONE => error "bn specified in a non-rec binding but not in bn list")
         | NONE =>
             let
@@ -312,7 +329,7 @@
                 if ((is_atom thy) o fastype_of) x then mk_single_atom x else
                 if ((is_atom_set thy) o fastype_of) x then mk_atoms x else
                 (* TODO we do not know what to do with non-atomizable things *)
-                @{term "{} :: atom set"}
+                @{term "{} :: atom set"};
               (* If i = j then we generate it only once *)
               val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs;
               val sub = fv_binds args relevant
diff -r 49bdb8d475df -r 7c8cd6eae8e2 Nominal/LFex.thy
--- a/Nominal/LFex.thy	Tue Mar 16 12:08:37 2010 +0100
+++ b/Nominal/LFex.thy	Tue Mar 16 15:27:47 2010 +0100
@@ -5,11 +5,11 @@
 atom_decl name
 atom_decl ident
 
-ML {* val cheat_fv_rsp = ref false *}
-ML {* val cheat_const_rsp = ref false *}
-ML {* val cheat_equivp = ref false *}
-ML {* val cheat_fv_eqvt = ref false *}
-ML {* val cheat_alpha_eqvt = ref false *}
+ML {* val _ = cheat_fv_rsp := false *}
+ML {* val _ = cheat_const_rsp := false *}
+ML {* val _ = cheat_equivp := false *}
+ML {* val _ = cheat_fv_eqvt := false *}
+ML {* val _ = cheat_alpha_eqvt := false *}
 
 nominal_datatype kind =
     Type
diff -r 49bdb8d475df -r 7c8cd6eae8e2 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Tue Mar 16 12:08:37 2010 +0100
+++ b/Nominal/Parser.thy	Tue Mar 16 15:27:47 2010 +0100
@@ -336,12 +336,6 @@
   val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
-  fun alpha_eqvt_tac' _ =
-    if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
-    else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1
-  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy4;
-  val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
-  val _ = map tracing (map PolyML.makestring alpha_eqvt)
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val fv_eqvt_tac =
     if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy)
@@ -351,6 +345,12 @@
   val lthy6 = lthy6a;
   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
+  fun alpha_eqvt_tac' _ =
+    if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
+    else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1
+  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy6;
+  val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
+  val _ = map tracing (map PolyML.makestring alpha_eqvt)
   val alpha_equivp_loc = 
     if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn
     else build_equivps alpha_ts_loc induct alpha_induct_loc
diff -r 49bdb8d475df -r 7c8cd6eae8e2 Nominal/Term5.thy
--- a/Nominal/Term5.thy	Tue Mar 16 12:08:37 2010 +0100
+++ b/Nominal/Term5.thy	Tue Mar 16 15:27:47 2010 +0100
@@ -43,6 +43,7 @@
 lemma fv_rtrm5_rlts_eqvt[eqvt]:
   "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"
   "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"
+  "pi \<bullet> (fv_rbv5 l) = fv_rbv5 (pi \<bullet> l)"
   apply (induct x and l)
   apply (simp_all add: eqvts atom_eqvt)
   done
@@ -57,8 +58,6 @@
 lemma alpha5_reflp:
 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)"
 apply (rule rtrm5_rlts.induct)
-thm rtrm5_rlts.induct
- alpha_rtrm5_alpha_rlts_alpha_rbv5.induct
 apply (simp_all add: alpha5_inj)
 apply (rule_tac x="0::perm" in exI)
 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm)
@@ -69,8 +68,6 @@
 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)"
 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
-thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct
-thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros
 apply (simp_all add: alpha5_inj)
 sorry
 
@@ -95,6 +92,7 @@
  |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
  |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_bv5", @{term fv_rbv5}))
  |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))
  |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5})))
 *}
@@ -102,14 +100,14 @@
 
 lemma alpha5_rfv:
   "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
-  "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m))"
-  "(alpha_rbv5 a b c \<Longrightarrow> True)"
+  "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m \<and> fv_rbv5 l = fv_rbv5 m))"
+  "(alpha_rbv5 0 b c \<Longrightarrow> fv_rbv5 b = fv_rbv5 c)"
   apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
-  apply(simp_all)
+  apply(simp_all add: eqvts)
   apply(simp add: alpha_gen)
   apply(clarify)
-  apply(simp_all)
-  sorry (* works for non-rec *)
+  apply(simp)
+  sorry
 
 lemma bv_list_rsp:
   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"
@@ -121,6 +119,7 @@
 
 lemma [quot_respect]:
   "(alpha_rlts ===> op =) fv_rlts fv_rlts"
+  "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5"
   "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"
   "(alpha_rlts ===> op =) rbv5 rbv5"
   "(op = ===> alpha_rtrm5) rVr5 rVr5"
@@ -173,12 +172,14 @@
 
 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
 lemmas bv5[simp] = rbv5.simps[quot_lifted]
-lemmas fv_trm5_lts[simp] = fv_rtrm5_fv_rlts.simps[quot_lifted]
+lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted]
+lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted]
 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
-apply (simp add: alpha5_INJ)
+thm alpha5_INJ
+apply (simp only: alpha5_INJ)
 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply (simp_all add: alpha_gen)
 apply (simp add: permute_trm5_lts fresh_star_def)
diff -r 49bdb8d475df -r 7c8cd6eae8e2 Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 16 12:08:37 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 16 15:27:47 2010 +0100
@@ -6,8 +6,9 @@
 
 atom_decl name
 
-ML {* val cheat_alpha_eqvt = ref false *}
-ML {* val cheat_fv_eqvt = ref false *}
+ML {* val _ = cheat_alpha_eqvt := false *}
+ML {* val _ = cheat_fv_eqvt := false *}
+ML {* val _ = recursive := false *}
 
 (*
 nominal_datatype lam =
@@ -60,7 +61,10 @@
 lemma alpha_bi:
   shows "alpha_bi pi b b' = True"
 apply(induct b rule: lam_bp_inducts(2))
-sorry
+apply(simp_all)
+apply(induct b' rule: lam_bp_inducts(2))
+apply (simp_all add: lam_bp_inject)
+done
 
 lemma fv_bi:
   shows "fv_bi b = {}"