# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1281233558 -28800
# Node ID 9294d7cec5e27662fc1b298c5023af8f9aa8594a
# Parent  ea143c806db6b4ae0c49c1881b607be4b1970f1e
proved rsp-helper lemmas of size functions

diff -r ea143c806db6 -r 9294d7cec5e2 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Sat Jul 31 02:10:42 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Sun Aug 08 10:12:38 2010 +0800
@@ -24,6 +24,8 @@
 thm alpha_sym_thms
 thm alpha_trans_thms
 thm size_eqvt
+thm size_simps
+thm size_rsp
 thm alpha_bn_imps
 thm distinct
 thm eq_iff
@@ -43,7 +45,6 @@
 term fv_trm
 term alpha_bn
 
-
 lemma exi_zero: "P 0 \<Longrightarrow> \<exists>(x::perm). P x" by auto
 
 ML {* 
@@ -77,7 +78,8 @@
   "(alpha_assg_raw ===> op =) bn_raw bn_raw"
   "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw"
   "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute"
-apply(simp_all add: alpha_bn_imps funs_rsp)
+  "(alpha_trm_raw ===> op =) size size"
+apply(simp_all add: alpha_bn_imps funs_rsp size_rsp)
 sorry
 
 ML {*
diff -r ea143c806db6 -r 9294d7cec5e2 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sat Jul 31 02:10:42 2010 +0100
+++ b/Nominal/NewParser.thy	Sun Aug 08 10:12:38 2010 +0800
@@ -322,7 +322,7 @@
   val raw_size_trms = map (fn ty => Const (@{const_name size}, ty --> @{typ nat})) all_raw_tys
   val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)
     |> `(fn thms => (length thms) div 2)
-    |> (uncurry drop)
+    |> uncurry drop
   
 
   (* definitions of raw permutations *)
@@ -442,6 +442,9 @@
   val raw_funs_rsp = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
     raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
 
+  val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
+    (raw_size_thms @ raw_size_eqvt) lthy6
+
 
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
@@ -504,6 +507,8 @@
      ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
      ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp)
      ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt)
+     ||>> Local_Theory.note ((@{binding "size_simps"}, []), raw_size_thms)
+     ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp)
      ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms)
      ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms)
   
diff -r ea143c806db6 -r 9294d7cec5e2 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Sat Jul 31 02:10:42 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Sun Aug 08 10:12:38 2010 +0800
@@ -27,6 +27,7 @@
   val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list
   val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> 
     term list -> thm -> thm list -> Proof.context -> thm list
+  val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
 end
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
@@ -621,5 +622,24 @@
     (K (asm_full_simp_tac ss)) ctxt
 end
 
+(* helper lemmas for respectfulness for size *)
+
+fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt =
+let
+  val arg_tys = map (domain_type o fastype_of) all_alpha_trms
+
+  fun mk_prop ty (x, y) = HOLogic.mk_eq 
+    (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y)
+
+  val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys 
+  
+  val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel.simps 
+    permute_prod_def prod.cases prod.recs})
+
+  val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss
+in
+  alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt
+end
+
 end (* structure *)
 
diff -r ea143c806db6 -r 9294d7cec5e2 Slides/document/root.tex
--- a/Slides/document/root.tex	Sat Jul 31 02:10:42 2010 +0100
+++ b/Slides/document/root.tex	Sun Aug 08 10:12:38 2010 +0800
@@ -109,12 +109,22 @@
 \chardef\isachardoublequoteclose=`\"%
 \chardef\isacharbackquoteopen=`\`%
 \chardef\isacharbackquoteclose=`\`%
+
+\let\oldisachardoublequoteopen=\isachardoublequoteopen
+\let\oldisachardoublequoteclose=\isachardoublequoteclose
+\let\oldisacharbackquoteopen=\isacharbackquoteopen
+\let\oldisacharbackquoteclose=\isacharbackquoteclose
+\newenvironment{innerdouble}%
+   {\oldisachardoublequoteopen \color{isacol:green}}%
+   {\color{isacol:black} \oldisachardoublequoteclose}
 \newenvironment{innersingle}%
-{\isacharbackquoteopen\color{isacol:green}}%
-{\color{isacol:black}\isacharbackquoteclose}
-\newenvironment{innerdouble}%
-{\isachardoublequoteopen\color{isacol:green}}%
-{\color{isacol:black}\isachardoublequoteclose}
+{\oldisacharbackquoteopen\color{isacol:green}}%
+{\color{isacol:black}\oldisacharbackquoteclose}
+
+\renewcommand{\isachardoublequoteopen}{\egroup\begin{innerdouble}\bgroup}
+\renewcommand{\isachardoublequoteclose}{\egroup\end{innerdouble}\bgroup}
+\renewcommand{\isacharbackquoteopen}{\egroup\begin{innersingle}\bgroup}
+\renewcommand{\isacharbackquoteclose}{\egroup\end{innersingle}\bgroup}
 
 %% misc
 \newcommand{\gb}[1]{\textcolor{isacol:green}{#1}}