# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256797752 -3600
# Node ID 38810e1df801d25e1d3a6eb29b4a934bf146075a
# Parent  c643938b846ae5c4ee8cadaf40163ab5ec5cb896# Parent  268a727b0f10ae7b391fab512f4f328eb66c1006
merged

diff -r 268a727b0f10 -r 38810e1df801 FSet.thy
--- a/FSet.thy	Wed Oct 28 18:08:38 2009 +0100
+++ b/FSet.thy	Thu Oct 29 07:29:12 2009 +0100
@@ -34,31 +34,32 @@
 thm "Rep_fset"
 thm "ABS_fset_def"
 
-ML {* @{term "Abs_fset"} *}
-local_setup {*
-  old_make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+quotient_def (for "'a fset")
+  EMPTY :: "'a fset"
+where
+  "EMPTY \<equiv> ([]::'a list)"
 
 term Nil
 term EMPTY
 thm EMPTY_def
 
-
-local_setup {*
-  old_make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+quotient_def (for "'a fset")
+  INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fet"
+where
+  "INSERT \<equiv> op #"
 
 term Cons
 term INSERT
 thm INSERT_def
 
-local_setup {*
-  old_make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+quotient_def (for "'a fset")
+  FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+where
+  "FUNION \<equiv> (op @)"
 
 term append
-term UNION
-thm UNION_def
+term FUNION
+thm FUNION_def
 
 thm QUOTIENT_fset
 
@@ -77,13 +78,14 @@
   card1_nil: "(card1 []) = 0"
 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
 
-local_setup {*
-  old_make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+quotient_def (for "'a fset")
+  CARD :: "'a fset \<Rightarrow> nat"
+where
+  "CARD \<equiv> card1"
 
 term card1
-term card
-thm card_def
+term CARD
+thm CARD_def
 
 (* text {*
  Maybe make_const_def should require a theorem that says that the particular lifted function
@@ -142,14 +144,21 @@
   apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1)
   done
 
-local_setup {*
-  old_make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+quotient_def (for "'a fset")
+  IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool"
+where
+  "IN \<equiv> membship"
 
 term membship
 term IN
 thm IN_def
 
+(* FIXME: does not work yet 
+quotient_def (for "'a fset")
+  FOLD :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
+where
+  "FOLD \<equiv> fold1"
+*)
 local_setup {*
   old_make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
@@ -158,6 +167,7 @@
 term fold
 thm fold_def
 
+(* FIXME: does not work yet for all types*)
 quotient_def (for "'a fset")
   fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
@@ -167,6 +177,19 @@
 term fmap
 thm fmap_def
 
+ML {* val fset_defs = @{thms EMPTY_def IN_def FUNION_def card_def INSERT_def fmap_def fold_def} *}
+(* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
+
+ML {*
+  val consts = [@{const_name "Nil"}, @{const_name "Cons"},
+                @{const_name "membship"}, @{const_name "card1"},
+                @{const_name "append"}, @{const_name "fold1"},
+                @{const_name "map"}];
+*}
+
+(* FIXME: does not work anymore :o( *)
+ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
+
 lemma memb_rsp:
   fixes z
   assumes a: "list_eq x y"
diff -r 268a727b0f10 -r 38810e1df801 LamEx.thy
--- a/LamEx.thy	Wed Oct 28 18:08:38 2009 +0100
+++ b/LamEx.thy	Thu Oct 29 07:29:12 2009 +0100
@@ -14,7 +14,7 @@
 where
   a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
-| a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
+| a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
 
 quotient lam = rlam / alpha
 apply -
@@ -22,16 +22,56 @@
 
 print_quotients
 
-local_setup {*
-  old_make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
-  old_make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
-  old_make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd
-*}
+quotient_def (for lam)
+  Var :: "name \<Rightarrow> lam"
+where
+  "Var \<equiv> rVar"
+
+quotient_def (for lam)
+  App :: "lam \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "App \<equiv> rApp"
+
+quotient_def (for lam)
+  Lam :: "name \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "Lam \<equiv> rLam"
 
 thm Var_def
 thm App_def
 thm Lam_def
 
+(* definition of overloaded permutation function *)
+(* for the lifted type lam                       *)
+overloading
+  perm_lam    \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"   (unchecked)
+begin
+
+quotient_def (for lam)
+  perm_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"
+
+end
+
+thm perm_lam_def
+
+(* lemmas that need to lift *)
+lemma
+  fixes pi::"'x prm"
+  shows "(pi\<bullet>Var a) = Var (pi\<bullet>a)"
+  sorry
+
+lemma
+  fixes pi::"'x prm"
+  shows "(pi\<bullet>App t1 t2) = App (pi\<bullet>t1) (pi\<bullet>t2)"
+  sorry
+
+lemma
+  fixes pi::"'x prm"
+  shows "(pi\<bullet>Lam a t) = Lam (pi\<bullet>a) (pi\<bullet>t)"
+  sorry
+
 lemma real_alpha:
   assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s"
   shows "Lam a t = Lam b s"
@@ -43,9 +83,28 @@
 
 (* Construction Site code *)
 
-lemma perm_rsp: "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>" sorry
-lemma fresh_rsp: "(op = ===> (alpha ===> op =)) fresh fresh" sorry
-lemma rLam_rsp: "(op = ===> (alpha ===> alpha)) rLam rLam" sorry
+lemma perm_rsp: "op = ===> alpha ===> alpha op \<bullet> op \<bullet>"
+  apply(auto)
+  (* this is propably true if some type conditions are imposed ;o) *)
+  sorry
+
+lemma fresh_rsp: "op = ===> (alpha ===> op =) fresh fresh" 
+  apply(auto)
+  (* this is probably only true if some type conditions are imposed *)
+  sorry
+
+lemma rLam_rsp: "op = ===> (alpha ===> alpha) rLam rLam"
+  apply(auto)
+  apply(rule a3)
+  apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
+  apply(rule sym)
+  apply(rule trans)
+  apply(rule pt_name3)
+  apply(rule at_ds1[OF at_name_inst])
+  apply(simp add: pt_name1)
+  apply(assumption)
+  apply(simp add: abs_fresh)
+  done
 
 ML {* val defs = @{thms Var_def App_def Lam_def} *}
 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}]; *}
diff -r 268a727b0f10 -r 38810e1df801 QuotTest.thy
--- a/QuotTest.thy	Wed Oct 28 18:08:38 2009 +0100
+++ b/QuotTest.thy	Thu Oct 29 07:29:12 2009 +0100
@@ -81,21 +81,21 @@
 *}
 
 ML {*
-  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
+  get_fun repF [(@{typ qt}, @{typ qt})] @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
   |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
 *}
 
 ML {*
-  get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}
+  get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "qt * nat"}
   |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
 *}
 
 ML {*
-  get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
+  get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
   |> fst
   |> Syntax.pretty_term @{context}
   |> Pretty.string_of
@@ -111,11 +111,20 @@
 *}
 *)
 
-local_setup {*
-  make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
-  make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
-  make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
-*}
+quotient_def (for qt)
+  VR ::"string \<Rightarrow> qt"
+where
+  "VR \<equiv> vr"
+
+quotient_def (for qt)
+  AP ::"qt list \<Rightarrow> qt"
+where
+  "AP \<equiv> ap"
+
+quotient_def (for qt)
+  LM ::"string \<Rightarrow> qt \<Rightarrow> qt"
+where
+  "LM \<equiv> lm"
 
 term vr
 term ap
@@ -141,11 +150,21 @@
 print_quotients
 print_theorems
 
-local_setup {*
-  make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
-  make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
-  make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
-*}
+
+quotient_def (for "'a qt'")
+  VR' ::"string \<Rightarrow> 'a qt"
+where
+  "VR' \<equiv> vr'"
+
+quotient_def (for "'a qt'")
+  AP' ::"('a qt') * ('a qt') \<Rightarrow> 'a qt"
+where
+  "AP' \<equiv> ap'"
+
+quotient_def (for "'a qt'")
+  LM' ::"'a \<Rightarrow> string \<Rightarrow> 'a qt'"
+where
+  "LM' \<equiv> lm'"
 
 term vr'
 term ap'