# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1307688349 -32400
# Node ID a99f488a96bbc7c97efd813d4e33ebf0657a9349
# Parent  aa76e2bea82cd4f7208d90e89d0f4c1ddaf12d06
Optimized proofs and removed some garbage.

diff -r aa76e2bea82c -r a99f488a96bb Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Fri Jun 10 15:31:14 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Fri Jun 10 15:45:49 2011 +0900
@@ -10,68 +10,30 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
-lemma cheat: "P" sorry
-
-thm lam.strong_exhaust
-
-lemma lam_strong_exhaust2:
-  "\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; 
-    \<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P;
-    \<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P;
-    finite (supp c)\<rbrakk>
-    \<Longrightarrow> P"
-sorry
-
-abbreviation
-  "FCB f \<equiv> \<forall>x t r. atom x \<sharp> f x t r" 
-
 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
   frees_set :: "lam \<Rightarrow> atom set"
 where
   "frees_set (Var x) = {atom x}"
 | "frees_set (App t1 t2) = frees_set t1 \<union> frees_set t2"
 | "frees_set (Lam [x]. t) = (frees_set t) - {atom x}"
-apply(simp add: eqvt_def frees_set_graph_def)
-apply (rule, perm_simp, rule)
-apply(erule frees_set_graph.induct)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(rule_tac y="x" in lam.exhaust)
-apply(auto)[6]
-apply(simp)
-apply(simp)
-apply(simp)
-apply (erule Abs_lst1_fcb)
-apply(simp add: fresh_def)
-apply(subst supp_of_finite_sets)
-apply(simp)
-apply(simp add: supp_atom)
-apply(simp add: fresh_def)
-apply(subst supp_of_finite_sets)
-apply(simp)
-apply(simp add: supp_atom)
-apply(subst  supp_finite_atom_set[symmetric])
-apply(simp)
-apply(simp add: fresh_def[symmetric])
-apply(rule fresh_eqvt_at)
-apply(assumption)
-apply(simp add: finite_supp)
-apply(simp)
-apply(simp add: eqvt_at_def eqvts)
-apply(simp)
-done
+  apply(simp add: eqvt_def frees_set_graph_def)
+  apply(rule, perm_simp, rule)
+  apply(erule frees_set_graph.induct)
+  apply(auto)[9]
+  apply(rule_tac y="x" in lam.exhaust)
+  apply(auto)[3]
+  apply(simp)
+  apply(erule Abs_lst1_fcb)
+  apply(simp_all add: fresh_minus_atom_set)
+  apply(erule fresh_eqvt_at)
+  apply(simp_all add: finite_supp eqvt_at_def eqvts)
+  done
 
 termination 
   by (relation "measure size") (auto simp add: lam.size)
 
-thm frees_set.simps
-thm frees_set.induct
-
 lemma "frees_set t = supp t"
-apply(induct rule: frees_set.induct)
-apply(simp_all add: lam.supp supp_at_base)
-done
+  by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base)
 
 lemma fresh_fun_eqvt_app3:
   assumes a: "eqvt f"
@@ -89,7 +51,7 @@
        and fcb: "\<forall>x t r. atom x \<sharp> f3 x t r"
 begin
 
-nominal_primrec 
+nominal_primrec
   f :: "lam \<Rightarrow> ('a::pt)"
 where
   "f (Var x) = f1 x"
@@ -223,11 +185,8 @@
   by (relation "measure size") (simp_all add: lam.size)
 
 text {* a small test lemma *}
-lemma
-  shows "supp t = set (frees_lst t)"
-apply(induct t rule: frees_lst.induct)
-apply(simp_all add: lam.supp supp_at_base)
-done
+lemma shows "supp t = set (frees_lst t)"
+  by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base)
 
 text {* capture - avoiding substitution *}
 
@@ -263,26 +222,23 @@
 
 lemma forget:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
-apply(nominal_induct t avoiding: x s rule: lam.strong_induct)
-apply(auto simp add: lam.fresh fresh_at_base)
-done
+  by (nominal_induct t avoiding: x s rule: lam.strong_induct)
+     (auto simp add: lam.fresh fresh_at_base)
 
 text {* same lemma but with subst.induction *}
 lemma forget2:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
-apply(induct t x s rule: subst.induct)
-apply(auto simp add: lam.fresh fresh_at_base fresh_Pair)
-done
+  by (induct t x s rule: subst.induct)
+     (auto simp add: lam.fresh fresh_at_base fresh_Pair)
 
 lemma fresh_fact:
   fixes z::"name"
   assumes a: "atom z \<sharp> s"
-  and b: "z = y \<or> atom z \<sharp> t"
+      and b: "z = y \<or> atom z \<sharp> t"
   shows "atom z \<sharp> t[y ::= s]"
-using a b
-apply (nominal_induct t avoiding: z y s rule: lam.strong_induct)
-apply (auto simp add: lam.fresh fresh_at_base)
-done
+  using a b
+  by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
+      (auto simp add: lam.fresh fresh_at_base)
 
 lemma substitution_lemma:  
   assumes a: "x \<noteq> y" "atom x \<sharp> u"
@@ -497,12 +453,7 @@
 
 lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs"
   unfolding fresh_def supp_set[symmetric]
-  apply (induct xs)
-  apply (simp add: supp_set_empty)
-  apply simp
-  apply auto
-  apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base)
-  done
+  by (induct xs) (auto simp add: supp_of_finite_insert supp_at_base supp_set_empty)
 
 fun
   vindex :: "name list \<Rightarrow> name \<Rightarrow> nat \<Rightarrow> db option" 
@@ -549,12 +500,10 @@
   apply auto
   done
 
-(*
 lemma db_trans_test:
   assumes a: "y \<noteq> x"
-  shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"
+  shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"
   using a by simp
-*)
 
 abbreviation
   mbind :: "'a option => ('a => 'b option) => 'b option"  ("_ \<guillemotright>= _" [65,65] 65) 
@@ -654,6 +603,8 @@
 apply rule
 apply simp
 oops (* can this be defined ? *)
+  (* Yes, if "sub" is a constant. *)
+
 
 text {* tests of functions containing if and case *}
 
@@ -744,19 +695,6 @@
 apply (rule, perm_simp, rule)
 oops
 
-(* function tests *)
-
-(* similar problem with function package *)
-function
-  f :: "int list \<Rightarrow> int"
-where
-  "f [] = 0"
-| "f [e] = e"
-| "f (l @ m) = f l + f m"
-  apply(simp_all)
-oops
-
-