# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268835183 -3600
# Node ID 2ca8e43b53c576f4b1907bec97762e4d7cd4c2a1
# Parent  4d01ab140f237dbed06f15efd95d4f04e5843431
added partial proof for the strong induction principle

diff -r 4d01ab140f23 -r 2ca8e43b53c5 Nominal/Test.thy
--- a/Nominal/Test.thy	Wed Mar 17 11:54:22 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 17 15:13:03 2010 +0100
@@ -6,10 +6,103 @@
 
 atom_decl name
 
+(* maybe should be added to Infinite.thy *)
+lemma infinite_Un:
+  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+  by simp
+
 ML {* val _ = cheat_alpha_eqvt := false *}
 ML {* val _ = cheat_fv_eqvt := false *}
 ML {* val _ = recursive := false *}
 
+nominal_datatype lm =
+  Vr "name"
+| Ap "lm" "lm"
+| Lm x::"name" l::"lm"  bind x in l
+
+lemma finite_fv:
+  shows "finite (fv_lm t)"
+apply(induct t rule: lm_induct)
+apply(simp_all add: lm_fv)
+done
+
+lemma supp_fn:
+  shows "supp t = fv_lm t"
+apply(induct t rule: lm_induct)
+apply(simp_all add: lm_fv)
+apply(simp only: supp_def)
+apply(simp only: lm_perm)
+apply(simp only: lm_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: lm_perm)
+apply(simp only: lm_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(rule_tac t="supp (Lm name lm_raw)" and s="supp (Abs {atom name} lm_raw)" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: lm_perm)
+apply(simp only: permute_ABS)
+apply(simp only: lm_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)
+done
+
+lemmas supp_fn' = lm_fv[simplified supp_fn[symmetric]]
+
+lemma obtain_atom_ex:
+  assumes fin: "finite (supp x)"
+  shows "\<exists>a. a \<sharp> x \<and> sort_of a = s"
+using obtain_atom[OF fin]
+unfolding fresh_def
+by blast
+
+lemma
+  assumes a0: "finite (supp c)"
+  and     a1: "\<And>name c. P c (Vr name)"
+  and     a2: "\<And>lm_raw1 lm_raw2 c. \<lbrakk>\<And>d. P d lm_raw1; \<And>d. P d lm_raw2\<rbrakk> \<Longrightarrow> P c (Ap lm_raw1 lm_raw2)"
+  and     a3: "\<And>name lm_raw c. \<lbrakk>\<And>d. P d lm_raw\<rbrakk> \<Longrightarrow> P c (Lm name lm_raw)"
+  shows "P c lm"
+proof -
+  have "\<And>p c. P c (p \<bullet> lm)"
+    apply(induct lm rule: lm_induct)
+    apply(simp only: lm_perm)
+    apply(rule a1)
+    apply(simp only: lm_perm)
+    apply(rule a2)
+    apply(assumption)
+    apply(assumption)
+    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm_raw)) 
+                          \<and> sort_of (atom new) = sort_of (atom name)")
+    apply(erule exE)
+    apply(rule_tac t="(p \<bullet> Lm name lm_raw)" and 
+                   s="((((atom (p \<bullet> name)) \<rightleftharpoons> (atom new)) + p) \<bullet> Lm name lm_raw)" in subst)
+    apply(simp)
+    apply(subst lm_perm)
+    apply(subst (2) lm_perm)
+    apply(rule swap_fresh_fresh)
+    apply(simp add: fresh_def)
+    apply(simp only: supp_fn')
+    apply(simp)
+    apply(simp add: fresh_Pair)
+    apply(simp add: lm_perm)
+    apply(rule a3)
+    apply(drule_tac x="(atom (p \<bullet> name) \<rightleftharpoons> atom new) + p" in meta_spec)
+    apply(simp)
+    sorry (* use at_set_avoiding *)    
+  then have "P c (0 \<bullet> lm)" by blast
+  then show "P c lm" by simp
+qed
+
+
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
@@ -33,11 +126,6 @@
 
 term "supp (x :: lam)"
 
-(* maybe should be added to Infinite.thy *)
-lemma infinite_Un:
-  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
-
 lemma bi_eqvt:
   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
   by (rule eqvts)
@@ -107,44 +195,6 @@
 
 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
 
-lemma supports_lam_bp:
-  "(supp (atom a)) supports (VAR a)"
-  "(supp t \<union> supp s) supports (APP t s)"
-  "(supp (atom a) \<union> supp t) supports (LAM a t)"
-  "(supp b \<union> supp t) supports (LET b t)"
-  "(supp (atom a) \<union> supp t) supports (BP a t)"
-apply -
-apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
-apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
-apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
-apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
-apply(tactic {* supports_tac @{thms lam_bp_perm} 1 *})
-done
-
-lemma finite_supp_lam_bp:
-  fixes lam::"lam" 
-  and   bp::"bp"
-  shows "finite (supp lam)"
-  and   "finite (supp bp)"
-apply(induct lam and bp rule: lam_bp_inducts)
-apply(rule supports_finite)
-apply(rule supports_lam_bp)
-apply(simp add: supp_atom)
-apply(rule supports_finite)
-apply(rule supports_lam_bp)
-apply(simp)
-apply(rule supports_finite)
-apply(rule supports_lam_bp)
-apply(simp add: supp_atom)
-apply(rule supports_finite)
-apply(rule supports_lam_bp)
-apply(simp)
-apply(rule supports_finite)
-apply(rule supports_lam_bp)
-apply(simp add: supp_atom)
-done
-
-
 ML {* val _ = cheat_alpha_eqvt := true *}
 ML {* val _ = recursive := true *}