# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271407300 -7200
# Node ID 310b7b768adfd394d765ec96d57458cbc5c6d0b4
# Parent  226b797868dca5a6aff1011d8ef553900ba1c902
Lifting in Term4.

diff -r 226b797868dc -r 310b7b768adf Nominal/Manual/Term4.thy
--- a/Nominal/Manual/Term4.thy	Fri Apr 16 10:18:16 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Fri Apr 16 10:41:40 2010 +0200
@@ -17,6 +17,7 @@
 (* there cannot be a clause for lists, as *)
 (* permutations are  already defined in Nominal (also functions, options, and so on) *)
 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term4.rtrm4") 1 *}
+print_theorems
 
 (* "repairing" of the permute function *)
 lemma repaired:
@@ -27,7 +28,8 @@
   done
 
 thm permute_rtrm4_permute_rtrm4_list.simps
-thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
+lemmas rawperm=permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
+
 
 local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4")
   [[[], [], [(NONE, 0, 1, AlphaGen)]], [[], []] ] [] *}
@@ -106,8 +108,6 @@
   (fn _ => asm_full_simp_tac (@{simpset} addsimps @{thms fv_rtrm4_rsp}) 1) *}
 print_theorems
 
-ML constr_rsp_tac
-
 local_setup {* snd o prove_const_rsp [] @{binding rVr4_rsp} [@{term rVr4}]
   (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *}
 local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}]
@@ -123,28 +123,10 @@
   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
 print_theorems
 
-lemma list_rel_rsp:
-  "\<lbrakk>\<forall>x y. R x y \<longrightarrow> (\<forall>a b. R a b \<longrightarrow> S x a = T y b); list_rel R x y; list_rel R a b\<rbrakk>
-    \<Longrightarrow> list_rel S x a = list_rel T y b"
-  sorry
-
-lemma[quot_respect]:
-  "((R ===> R ===> op =) ===> list_rel R ===> list_rel R ===> op =) list_rel list_rel"
-  by (simp add: list_rel_rsp)
+setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_append} *}
+print_theorems
 
-lemma[quot_preserve]:
-  assumes a: "Quotient R abs1 rep1"
-  shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_rel = list_rel"
-  apply (simp add: expand_fun_eq)
-  apply clarify
-  apply (induct_tac xa xb rule: list_induct2')
-  apply (simp_all add: Quotient_abs_rep[OF a])
-  done
 
-lemma[quot_preserve]:
-  assumes a: "Quotient R abs1 rep1"
-  shows "(list_rel ((rep1 ---> rep1 ---> id) R) l m) = (l = m)"
-  by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a])
 
 lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) =
   (trm4 = trm4a \<and> list_rel (op =) list lista)"
@@ -152,12 +134,6 @@
 
 thm bla[simplified list_rel_eq]
 
-lemma " (Lm4 name rtrm4 = Lm4 namea rtrm4a) =
- (\<exists>pi\<Colon>perm.
-     fv_trm4 rtrm4 - {atom name} = fv_trm4 rtrm4a - {atom namea} \<and>
-     (fv_trm4 rtrm4 - {atom name}) \<sharp>* pi \<and>
-     pi \<bullet> rtrm4 = rtrm4a \<and> pi \<bullet> {atom name} = {atom namea})"
-
 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(1)} *}
 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(2)} *}
 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(3)[unfolded alpha_gen]} *}