--- a/Nominal/Ex/Lambda.thy	Fri Apr 09 09:02:54 2010 -0700
+++ b/Nominal/Ex/Lambda.thy	Fri Apr 09 21:51:01 2010 +0200
@@ -4,12 +4,14 @@
 
 atom_decl name
 
-nominal_datatype lm =
-  Vr "name"
-| Ap "lm" "lm"
-| Lm x::"name" l::"lm"  bind x in l
+nominal_datatype lam =
+  Var "name"
+| App "lam" "lam"
+| Lam x::"name" l::"lam"  bind x in l
 
-lemmas supp_fn' = lm.fv[simplified lm.supp]
+lemmas supp_fn' = lam.fv[simplified lam.supp]
+
+section {* Strong Induction Principles*}
 
 (* 
   Old way of establishing strong induction
@@ -17,31 +19,31 @@
 *)
 lemma
   fixes c::"'a::fs"
-  assumes a1: "\<And>name c. P c (Vr name)"
-  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
-  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
-  shows "P c lm"
+  assumes a1: "\<And>name c. P c (Var name)"
+  and     a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
+  and     a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
+  shows "P c lam"
 proof -
-  have "\<And>p. P c (p \<bullet> lm)"
-    apply(induct lm arbitrary: c rule: lm.induct)
-    apply(simp only: lm.perm)
+  have "\<And>p. P c (p \<bullet> lam)"
+    apply(induct lam arbitrary: c rule: lam.induct)
+    apply(simp only: lam.perm)
     apply(rule a1)
-    apply(simp only: lm.perm)
+    apply(simp only: lam.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))")
+    apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lam (p \<bullet> name) (p \<bullet> lam))")
     defer
     apply(simp add: fresh_def)
-    apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base)
+    apply(rule_tac X="supp (c, Lam (p \<bullet> name) (p \<bullet> lam))" in obtain_at_base)
     apply(simp add: supp_Pair finite_supp)
     apply(blast)
     apply(erule exE)
-    apply(rule_tac t="p \<bullet> Lm name lm" and 
-                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
-    apply(simp del: lm.perm)
-    apply(subst lm.perm)
-    apply(subst (2) lm.perm)
+    apply(rule_tac t="p \<bullet> Lam name lam" and 
+                   s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lam name lam" in subst)
+    apply(simp del: lam.perm)
+    apply(subst lam.perm)
+    apply(subst (2) lam.perm)
     apply(rule flip_fresh_fresh)
     apply(simp add: fresh_def)
     apply(simp only: supp_fn')
@@ -53,8 +55,8 @@
     apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
     apply(simp)
     done
-  then have "P c (0 \<bullet> lm)" by blast
-  then show "P c lm" by simp
+  then have "P c (0 \<bullet> lam)" by blast
+  then show "P c lam" by simp
 qed
 
 (* 
@@ -63,25 +65,25 @@
 *)
 lemma
   fixes c::"'a::fs"
-  assumes a1: "\<And>name c. P c (Vr name)"
-  and     a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
-  and     a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
-  shows "P c lm"
+  assumes a1: "\<And>name c. P c (Var name)"
+  and     a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)"
+  and     a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)"
+  shows "P c lam"
 proof -
-  have "\<And>p. P c (p \<bullet> lm)"
-    apply(induct lm arbitrary: c rule: lm.induct)
-    apply(simp only: lm.perm)
+  have "\<And>p. P c (p \<bullet> lam)"
+    apply(induct lam arbitrary: c rule: lam.induct)
+    apply(simp only: lam.perm)
     apply(rule a1)
-    apply(simp only: lm.perm)
+    apply(simp only: lam.perm)
     apply(rule a2)
     apply(assumption)
     apply(assumption)
-    apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q")
+    apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lam name lam) \<sharp>* q")
     apply(erule exE)
-    apply(rule_tac t="p \<bullet> Lm name lm" and 
-                   s="q \<bullet> p \<bullet> Lm name lm" in subst)
+    apply(rule_tac t="p \<bullet> Lam name lam" and 
+                   s="q \<bullet> p \<bullet> Lam name lam" in subst)
     defer
-    apply(simp add: lm.perm)
+    apply(simp add: lam.perm)
     apply(rule a3)
     apply(simp add: eqvts fresh_star_def)
     apply(drule_tac x="q + p" in meta_spec)
@@ -90,15 +92,172 @@
     apply(simp add: finite_supp)
     apply(simp add: finite_supp)
     apply(simp add: finite_supp)
-    apply(simp only: lm.perm atom_eqvt)
+    apply(simp only: lam.perm atom_eqvt)
     apply(simp add: fresh_star_def fresh_def supp_fn')
     apply(rule supp_perm_eq)
     apply(simp)
     done
-  then have "P c (0 \<bullet> lm)" by blast
-  then show "P c lm" by simp
+  then have "P c (0 \<bullet> lam)" by blast
+  then show "P c lam" by simp
 qed
 
+section {* size function *}
+
+lemma size_eqvt_raw:
+  fixes t::"lam_raw"
+  shows "size (pi \<bullet> t)  = size t"
+  apply (induct rule: lam_raw.inducts)
+  apply simp_all
+  done
+
+instantiation lam :: size 
+begin
+
+quotient_definition
+  "size_lam :: lam \<Rightarrow> nat"
+is
+  "size :: lam_raw \<Rightarrow> nat"
+
+lemma size_rsp:
+  "alpha_lam_raw x y \<Longrightarrow> size x = size y"
+  apply (induct rule: alpha_lam_raw.inducts)
+  apply (simp_all only: lam_raw.size)
+  apply (simp_all only: alphas)
+  apply clarify
+  apply (simp_all only: size_eqvt_raw)
+  done
+
+lemma [quot_respect]:
+  "(alpha_lam_raw ===> op =) size size"
+  by (simp_all add: size_rsp)
+
+lemma [quot_preserve]:
+  "(rep_lam ---> id) size = size"
+  by (simp_all add: size_lam_def)
+
+instance
+  by default
+
+end
+
+lemmas size_lam[simp] = 
+  lam_raw.size(4)[quot_lifted]
+  lam_raw.size(5)[quot_lifted]
+  lam_raw.size(6)[quot_lifted]
+
+(* is this needed? *)
+lemma [measure_function]: 
+  "is_measure (size::lam\<Rightarrow>nat)" 
+  by (rule is_measure_trivial)
+
+section {* Matching *}
+
+definition
+  MATCH :: "('c::pt \<Rightarrow> (bool * 'a::pt * 'b::pt)) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+  "MATCH M d x \<equiv> if (\<exists>!r. \<exists>q. M q = (True, x, r)) then (THE r. \<exists>q. M q = (True, x, r)) else d"
+
+(*
+lemma MATCH_eqvt:
+  shows "p \<bullet> (MATCH M d x) = MATCH (p \<bullet> M) (p \<bullet> d) (p \<bullet> x)"
+unfolding MATCH_def
+apply(perm_simp the_eqvt)
+apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+apply(simp)
+thm eqvts_raw 
+apply(subst if_eqvt)
+apply(subst ex1_eqvt)
+apply(subst permute_fun_def)
+apply(subst ex_eqvt)
+apply(subst permute_fun_def)
+apply(subst eq_eqvt)
+apply(subst permute_fun_app_eq[where f="M"])
+apply(simp only: permute_minus_cancel)
+apply(subst permute_prod.simps)
+apply(subst permute_prod.simps)
+apply(simp only: permute_minus_cancel)
+apply(simp only: permute_bool_def)
+apply(simp)
+apply(subst ex1_eqvt)
+apply(subst permute_fun_def)
+apply(subst ex_eqvt)
+apply(subst permute_fun_def)
+apply(subst eq_eqvt)
+
+apply(simp only: eqvts)
+apply(simp)
+apply(subgoal_tac "(p \<bullet> (\<exists>!r. \<exists>q. M q = (True, x, r))) = (\<exists>!r. \<exists>q. (p \<bullet> M) q = (True, p \<bullet> x, r))")
+apply(drule sym)
+apply(simp)
+apply(rule impI)
+apply(simp add: perm_bool)
+apply(rule trans)
+apply(rule pt_the_eqvt[OF pta at])
+apply(assumption)
+apply(simp add: pt_ex_eqvt[OF pt at])
+apply(simp add: pt_eq_eqvt[OF ptb at])
+apply(rule cheat)
+apply(rule trans)
+apply(rule pt_ex1_eqvt)
+apply(rule pta)
+apply(rule at)
+apply(simp add: pt_ex_eqvt[OF pt at])
+apply(simp add: pt_eq_eqvt[OF ptb at])
+apply(subst pt_pi_rev[OF pta at])
+apply(subst pt_fun_app_eq[OF pt at])
+apply(subst pt_pi_rev[OF pt at])
+apply(simp)
+done
+
+lemma MATCH_cng:
+  assumes a: "M1 = M2" "d1 = d2"
+  shows "MATCH M1 d1 x = MATCH M2 d2 x"
+using a by simp
+
+lemma MATCH_eq:
+  assumes a: "t = l x" "G x" "\<And>x'. t = l x' \<Longrightarrow> G x' \<Longrightarrow> r x' = r x"
+  shows "MATCH (\<lambda>x. (G x, l x, r x)) d t = r x"
+using a
+unfolding MATCH_def
+apply(subst if_P)
+apply(rule_tac a="r x" in ex1I)
+apply(rule_tac x="x" in exI)
+apply(blast)
+apply(erule exE)
+apply(drule_tac x="q" in meta_spec)
+apply(auto)[1]
+apply(rule the_equality)
+apply(blast)
+apply(erule exE)
+apply(drule_tac x="q" in meta_spec)
+apply(auto)[1]
+done
+
+lemma MATCH_eq2:
+  assumes a: "t = l x1 x2" "G x1 x2" "\<And>x1' x2'. t = l x1' x2' \<Longrightarrow> G x1' x2' \<Longrightarrow> r x1' x2' = r x1 x2"
+  shows "MATCH (\<lambda>(x1,x2). (G x1 x2, l x1 x2, r x1 x2)) d t = r x1 x2"
+sorry
+
+lemma MATCH_neq:
+  assumes a: "\<And>x. t = l x \<Longrightarrow> G x \<Longrightarrow> False"
+  shows "MATCH (\<lambda>x. (G x, l x, r x)) d t = d"
+using a
+unfolding MATCH_def
+apply(subst if_not_P)
+apply(blast)
+apply(rule refl)
+done
+
+lemma MATCH_neq2:
+  assumes a: "\<And>x1 x2. t = l x1 x2 \<Longrightarrow> G x1 x2 \<Longrightarrow> False"
+  shows "MATCH (\<lambda>(x1,x2). (G x1 x2, l x1 x2, r x1 x2)) d t = d"
+using a
+unfolding MATCH_def
+apply(subst if_not_P)
+apply(auto)
+done
+*)
+
 end