# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1293797579 0
# Node ID e8732350a29f9e375c2b518599d075312186f5a9
# Parent  e73bd379e8399c94d041be3eabb3f91cc607eaa4
added small example for strong inductions; functions still need a sorry

diff -r e73bd379e839 -r e8732350a29f Nominal/Ex/Height.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Height.thy	Fri Dec 31 12:12:59 2010 +0000
@@ -0,0 +1,103 @@
+theory Height
+  imports "../Nominal2"
+begin
+
+text {*  
+  A small problem suggested by D. Wang. It shows how
+  the height of a lambda-terms behaves under substitution.
+*}
+
+atom_decl name
+
+nominal_datatype lam = 
+    Var "name"
+  | App "lam" "lam"
+  | Lam x::"name" l::"lam" bind x in l ("Lam [_]._" [100,100] 100)
+
+thm lam.strong_induct
+
+text {* Definition of the height-function on lambda-terms. *} 
+
+function
+  height :: "lam \<Rightarrow> int"
+where
+  "height (Var x) = 1"
+| "height (App t1 t2) = (max (height t1) (height t2)) + 1"
+| "height (Lam [a].t) = (height t) + 1"
+  apply(rule_tac y="x" in lam.exhaust)
+  apply(simp_all)[3]
+  apply(simp add: lam.eq_iff)
+  apply(simp add: lam.distinct)
+  apply(simp add: lam.distinct)
+  apply(simp add: lam.eq_iff)
+  apply(simp add: lam.distinct)
+  apply(simp add: lam.eq_iff)
+  sorry
+
+termination
+  apply(relation "measure size")
+  apply(simp_all add: lam.size)
+  done
+
+text {* Definition of capture-avoiding substitution. *}
+
+function
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
+where
+  "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
+| "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
+| "\<lbrakk>atom x \<sharp> y; atom x \<sharp> t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
+apply(case_tac x)
+apply(simp)
+apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
+apply(simp_all)[3]
+apply(blast)
+apply(blast)
+apply(simp add: fresh_star_def fresh_Pair)
+apply(blast)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.distinct)
+apply(simp add: lam.distinct)
+apply(simp add: lam.eq_iff)
+apply(simp add: lam.distinct)
+apply(simp add: lam.eq_iff)
+sorry
+
+termination
+  apply(relation "measure (size o fst)")
+  apply(simp_all add: lam.size)
+  done
+
+text{* The next lemma is needed in the Var-case of the theorem below. *}
+
+lemma height_ge_one: 
+  shows "1 \<le> (height e)"
+apply(nominal_induct e rule: lam.strong_induct) 
+apply(simp_all)
+done
+
+text {* 
+  Unlike the proplem suggested by Wang, however, the 
+  theorem is here formulated entirely by using functions. 
+*}
+
+theorem height_subst:
+  shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')"
+proof (nominal_induct e avoiding: x e' rule: lam.strong_induct)
+  case (1 y)
+  have "1 \<le> height e'" by (rule height_ge_one)
+  then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp
+next
+  case (3 y e1)
+  have ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by fact
+  moreover
+  have vc: "atom y \<sharp> x" "atom y \<sharp> e'" by fact+ (* usual variable convention *)
+  ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp
+next    
+  case (2 e1 e2)
+  have ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" 
+  and  ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by fact+
+  then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'"  by simp 
+qed
+
+end
diff -r e73bd379e839 -r e8732350a29f Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Thu Dec 30 10:00:09 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Fri Dec 31 12:12:59 2010 +0000
@@ -1407,8 +1407,34 @@
   done
 
 
-section {* Fresh-Star *}
+section {* Freshness and Fresh-Star *}
+
+lemma fresh_Unit_elim: 
+  shows "(a \<sharp> () \<Longrightarrow> PROP C) \<equiv> PROP C"
+  by (simp add: fresh_Unit)
+
+lemma fresh_Pair_elim: 
+  shows "(a \<sharp> (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> a \<sharp> y \<Longrightarrow> PROP C)"
+  by rule (simp_all add: fresh_Pair)
 
+(* this rule needs to be added before the fresh_prodD is *)
+(* added to the simplifier with mksimps                  *) 
+lemma [simp]:
+  shows "a \<sharp> x1 \<Longrightarrow> a \<sharp> x2 \<Longrightarrow> a \<sharp> (x1, x2)"
+  by (simp add: fresh_Pair)
+
+lemma fresh_PairD:
+  shows "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> x"
+  and   "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> y"
+  by (simp_all add: fresh_Pair)
+
+ML {*
+  val mksimps_pairs = (@{const_name Nominal2_Base.fresh}, @{thms fresh_PairD}) :: mksimps_pairs;
+*}
+
+declaration {* fn _ =>
+  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
+*}
 
 text {* The fresh-star generalisation of fresh is used in strong
   induction principles. *}
@@ -1473,7 +1499,7 @@
   "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"
   by (simp add: fresh_star_def)
 
-lemma fresh_star_unit_elim: 
+lemma fresh_star_Unit_elim: 
   shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"
   by (simp add: fresh_star_def fresh_Unit) 
 
diff -r e73bd379e839 -r e8732350a29f Nominal/nominal_induct.ML
--- a/Nominal/nominal_induct.ML	Thu Dec 30 10:00:09 2010 +0000
+++ b/Nominal/nominal_induct.ML	Fri Dec 31 12:12:59 2010 +0000
@@ -24,11 +24,10 @@
 
 val split_all_tuples =
   Simplifier.full_simplify (HOL_basic_ss addsimps
-    @{thms split_conv split_paired_all unit_all_eq1})
-(* 
-     @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @
-     @{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim})
-*)
+    @{thms split_conv split_paired_all unit_all_eq1} @
+    @{thms fresh_Unit_elim fresh_Pair_elim} @
+    @{thms fresh_star_Unit_elim fresh_star_Pair_elim fresh_star_Un_elim} @
+    @{thms fresh_star_insert_elim fresh_star_empty_elim})
 
 
 (* prepare rule *)