# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268804973 -3600
# Node ID 4de35639fef056e095208f302e53bd0f03a2c7b9
# Parent  1850361efb8f545b4100e94f0d3edb77185e4386
added another supp-proof for the non-recursive case

diff -r 1850361efb8f -r 4de35639fef0 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Tue Mar 16 20:07:13 2010 +0100
+++ b/Nominal/Abs.thy	Wed Mar 17 06:49:33 2010 +0100
@@ -2,11 +2,27 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
 begin
 
+lemma permute_boolI:
+  fixes P::"bool"
+  shows "p \<bullet> P \<Longrightarrow> P"
+apply(simp add: permute_bool_def)
+done
+
+lemma permute_boolE:
+  fixes P::"bool"
+  shows "P \<Longrightarrow> p \<bullet> P"
+apply(simp add: permute_bool_def)
+done
+
 fun
   alpha_gen 
 where
   alpha_gen[simp del]:
-  "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> f x - bs = f y - cs \<and> (f x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y"
+  "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> 
+     f x - bs = f y - cs \<and> 
+     (f x - bs) \<sharp>* pi \<and> 
+     R (pi \<bullet> x) y \<and>
+     pi \<bullet> bs = cs"
 
 notation
   alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
@@ -23,7 +39,11 @@
   assumes a: "(bs, x) \<approx>gen R f p (cs, y)"
   and     b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
   shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
-  using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
+  using a b 
+  apply (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
+  apply(clarify)
+  apply(simp)
+  done
 
 lemma alpha_gen_trans:
   assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
@@ -60,6 +80,8 @@
   apply(simp add: fresh_star_def fresh_minus_perm)
   apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
   apply simp
+  apply(clarify)
+  apply(simp)
   apply(rule a)
   apply assumption
   done
@@ -76,10 +98,10 @@
   apply(simp add: fresh_star_plus)
   apply(drule_tac x="- pia \<bullet> sa" in spec)
   apply(drule mp)
-  apply(rotate_tac 4)
+  apply(rotate_tac 5)
   apply(drule_tac pi="- pia" in a)
   apply(simp)
-  apply(rotate_tac 6)
+  apply(rotate_tac 7)
   apply(drule_tac pi="pia" in a)
   apply(simp)
   done
@@ -102,7 +124,7 @@
   apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
   apply(subst permute_eqvt[symmetric])
   apply(simp)
-  done
+  sorry
 
 fun
   alpha_abs 
@@ -112,6 +134,8 @@
 notation
   alpha_abs ("_ \<approx>abs _")
 
+
+
 lemma alpha_abs_swap:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
@@ -346,23 +370,6 @@
 notation 
   alpha2 ("_ \<approx>abs2 _")
 
-lemma qq:
-  fixes S::"atom set"
-  assumes a: "supp p \<inter> S = {}"
-  shows "p \<bullet> S = S"
-using a
-apply(simp add: supp_perm permute_set_eq)
-apply(auto)
-apply(simp only: disjoint_iff_not_equal)
-apply(simp)
-apply (metis permute_atom_def_raw)
-apply(rule_tac x="(- p) \<bullet> x" in exI)
-apply(simp)
-apply(simp only: disjoint_iff_not_equal)
-apply(simp)
-apply(metis permute_minus_cancel)
-done
-
 lemma alpha_old_new:
   assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
   shows "({a}, x) \<approx>abs ({b}, y)"
@@ -385,6 +392,7 @@
 apply(simp)
 apply(simp)
 apply(simp add: permute_set_eq)
+apply(rule conjI)
 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])
 apply(simp add: permute_self)
 apply(simp add: Diff_eqvt supp_eqvt)
@@ -393,6 +401,7 @@
 apply(simp add: fresh_star_def fresh_def)
 apply(blast)
 apply(simp add: supp_swap)
+apply(simp add: eqvts)
 done
 
 lemma perm_zero:
@@ -532,9 +541,42 @@
 apply(simp add: zero)
 apply(rotate_tac 3)
 oops
-lemma tt:
-  "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
-oops
+
+lemma ii:
+  assumes "\<forall>x \<in> A. p \<bullet> x = x"
+  shows "p \<bullet> A = A"
+using assms
+apply(auto)
+apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_bound inf_Int_eq mem_def mem_permute_iff)
+apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_apply eqvt_bound eqvt_lambda inf_Int_eq mem_def mem_permute_iff permute_minus_cancel(2) permute_pure)
+done
+
+
+
+lemma alpha_abs_Pair:
+  shows "(bs, (x1, x2)) \<approx>gen (\<lambda>(x1,x2) (y1,y2). x1=y1 \<and> x2=y2) (\<lambda>(x,y). supp x \<union> supp y) p (cs, (y1, y2))
+         \<longleftrightarrow> ((bs, x1) \<approx>gen (op=) supp p (cs, y1) \<and> (bs, x2) \<approx>gen (op=) supp p (cs, y2))"         
+  apply(simp add: alpha_gen)
+  apply(simp add: fresh_star_def)
+  apply(simp add: ball_Un Un_Diff)
+  apply(rule iffI)
+  apply(simp)
+  defer
+  apply(simp)
+  apply(rule conjI)
+  apply(clarify)
+  apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
+  apply(rule sym)
+  apply(rule ii)
+  apply(simp add: fresh_def supp_perm)
+  apply(clarify)
+  apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
+  apply(simp add: fresh_def supp_perm)
+  apply(rule sym)
+  apply(rule ii)
+  apply(simp)
+  done
+
 
 lemma yy:
   assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
@@ -543,18 +585,6 @@
 apply (metis insert_Diff_single insert_absorb)
 done
 
-lemma permute_boolI:
-  fixes P::"bool"
-  shows "p \<bullet> P \<Longrightarrow> P"
-apply(simp add: permute_bool_def)
-done
-
-lemma permute_boolE:
-  fixes P::"bool"
-  shows "P \<Longrightarrow> p \<bullet> P"
-apply(simp add: permute_bool_def)
-done
-
 lemma kk:
   assumes a: "p \<bullet> x = y"
   shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"
diff -r 1850361efb8f -r 4de35639fef0 Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 16 20:07:13 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 17 06:49:33 2010 +0100
@@ -109,8 +109,95 @@
 
 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
 
+ML {* val _ = recursive := true *}
+
+nominal_datatype lam' =
+  VAR' "name"
+| APP' "lam'" "lam'"
+| LAM' x::"name" t::"lam'"  bind x in t
+| LET' bp::"bp'" t::"lam'"   bind "bi' bp" in t
+and bp' =
+  BP' "name" "lam'"
+binder
+  bi'::"bp' \<Rightarrow> atom set"
+where
+  "bi' (BP' x t) = {atom x}"
+
+thm lam'_bp'_fv
+thm lam'_bp'_inject[no_vars]
+thm lam'_bp'_bn
+thm lam'_bp'_perm
+thm lam'_bp'_induct
+thm lam'_bp'_inducts
+thm lam'_bp'_distinct
+ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
+
+lemma supp_fv:
+  shows "supp t = fv_lam' t" 
+  and "supp bp = fv_bp' bp"
+apply(induct t and bp rule: lam'_bp'_inducts)
+apply(simp_all add: lam'_bp'_fv)
+(* VAR case *)
+apply(simp only: supp_def)
+apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+(* APP case *)
+apply(simp only: supp_def)
+apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+(* LAM case *)
+apply(rule_tac t="supp (LAM' name lam'_raw)" and s="supp (Abs {atom name} lam'_raw)" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: lam'_bp'_perm)
+apply(simp only: permute_ABS)
+apply(simp only: lam'_bp'_inject)
+apply(simp only: Abs_eq_iff)
+apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
+apply(simp only: alpha_gen)
+apply(simp only: supp_eqvt[symmetric])
+apply(simp only: eqvts)
+apply(simp only: supp_Abs)
+(* LET case *)
+apply(rule_tac t="supp (LET' bp'_raw lam'_raw)" and 
+               s="supp (Abs (bi' bp'_raw) (bp'_raw, lam'_raw))" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: lam'_bp'_perm)
+apply(simp only: permute_ABS)
+apply(simp only: lam'_bp'_inject)
+apply(simp only: eqvts)
+apply(simp only: Abs_eq_iff)
+apply(rule Collect_cong)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(simp)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(simp)
+apply(rule Collect_cong)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(simp)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(simp)
+apply(rule ext)
+apply(rule sym)
+apply(subgoal_tac "fv_bp' = supp")
+apply(subgoal_tac "fv_lam' = supp")
+apply(simp)
+apply(rule trans)
+apply(rule alpha_abs_Pair[symmetric])
+apply(simp add: alpha_gen supp_Pair)
+oops
+
+thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
+
+
 text {* example 2 *}
 
+ML {* val _ = recursive := false  *}
 nominal_datatype trm' =
   Var "name"
 | App "trm'" "trm'"
@@ -134,11 +221,82 @@
 thm trm'_pat'_induct
 thm trm'_pat'_distinct
 
-(* compat should be
-compat (PN) pi (PN) == True
-compat (PS x) pi (PS x') == pi o x = x'
-compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2'
-*)
+lemma supp_fv_trm'_pat':
+  shows "supp t = fv_trm' t" 
+  and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp"
+apply(induct t and bp rule: trm'_pat'_inducts)
+apply(simp_all add: trm'_pat'_fv)
+(* VAR case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+(* APP case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+(* LAM case *)
+apply(rule_tac t="supp (Lam name trm'_raw)" and s="supp (Abs {atom name} trm'_raw)" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: permute_ABS)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: Abs_eq_iff)
+apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
+apply(simp only: alpha_gen)
+apply(simp only: supp_eqvt[symmetric])
+apply(simp only: eqvts)
+apply(simp only: supp_Abs)
+(* LET case *)
+apply(rule_tac t="supp (Let pat'_raw trm'_raw1 trm'_raw2)" 
+           and s="supp (Abs (f pat'_raw) trm'_raw2) \<union> supp trm'_raw1 \<union> fv_f pat'_raw" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: permute_ABS)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: eqvts)
+apply(simp only: Abs_eq_iff)
+apply(simp only: ex_simps)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+apply(simp only: alpha_gen)
+apply(simp only: supp_eqvt[symmetric])
+apply(simp only: eqvts)
+apply(blast)
+apply(simp add: supp_Abs)
+apply(blast)
+(* PN case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp)
+(* PS case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+apply(simp)
+(* PD case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+apply(simp only: supp_def[symmetric])
+apply(simp add: supp_at_base)
+done
+
+thm trm'_pat'_fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]]
 
 nominal_datatype trm0 =
   Var0 "name"