# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1276218162 -7200
# Node ID 08bbde090a17b07bfe9a05ef564fc9ff88574477
# Parent  4e5a7b606eab12a72e544dd2bb5463579dc48f1b
also symmetry

diff -r 4e5a7b606eab -r 08bbde090a17 Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Thu Jun 10 14:53:45 2010 +0200
+++ b/Nominal/Ex/CoreHaskell.thy	Fri Jun 11 03:02:42 2010 +0200
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 11]]
+declare [[STEPS = 12]]
 
 nominal_datatype tkind =
   KStar
@@ -85,6 +85,7 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
+
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm
diff -r 4e5a7b606eab -r 08bbde090a17 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Thu Jun 10 14:53:45 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Fri Jun 11 03:02:42 2010 +0200
@@ -2,10 +2,10 @@
 imports "../NewParser"
 begin
 
-
 atom_decl name
 
-declare [[STEPS = 11]]
+declare [[STEPS = 12]]
+
 
 nominal_datatype trm =
   Var "name"
@@ -14,6 +14,7 @@
 | Let a::"assg" t::"trm"  bind_set "bn a" in t
 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2
 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
+| Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 
 and assg =
   As "name" "name" "trm" "name"
 binder
@@ -22,6 +23,48 @@
   "bn (As x y t z) = {atom x}"
 
 
+lemma
+  shows "alpha_trm_raw x x"
+  and "alpha_assg_raw y y"
+  and "alpha_bn_raw y y"
+apply(induct rule: trm_raw_assg_raw.inducts)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule refl)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(assumption)
+apply(assumption)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule_tac x="0" in exI)
+apply(rule alpha_gen_refl)
+apply(assumption)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule_tac x="0" in exI)
+apply(rule alpha_gen_refl)
+apply(assumption)
+apply(assumption)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule_tac x="0" in exI)
+apply(rule alpha_gen_refl)
+apply(simp only: prod_alpha_def split_conv prod_rel.simps)
+apply(simp)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule_tac x="0" in exI)
+apply(rule alpha_gen_refl)
+apply(simp only: prod_alpha_def split_conv prod_rel.simps)
+apply(simp)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule refl)
+apply(rule refl)
+apply(assumption)
+apply(rule refl)
+apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+apply(rule refl)
+apply(assumption)
+apply(rule refl)
+done
+
+
+
 thm trm_assg.fv
 thm trm_assg.supp
 thm trm_assg.eq_iff
diff -r 4e5a7b606eab -r 08bbde090a17 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Thu Jun 10 14:53:45 2010 +0200
+++ b/Nominal/NewParser.thy	Fri Jun 11 03:02:42 2010 +0200
@@ -326,7 +326,7 @@
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatypes *)
-
+  val _ = warning "Definition of raw datatypes";
   val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
     if get_STEPS lthy > 0 
     then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
@@ -347,6 +347,7 @@
   val exhaust_thms = map #exhaust dtinfos;
 
   (* definitions of raw permutations *)
+  val _ = warning "Definition of raw permutations";
   val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) =
     if get_STEPS lthy0 > 1 
     then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0
@@ -360,6 +361,7 @@
   val thy_name = Context.theory_name thy
 
   (* definition of raw fv_functions *)
+  val _ = warning "Definition of raw fv-functions";
   val lthy3 = Theory_Target.init NONE thy;
 
   val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
@@ -367,25 +369,25 @@
     then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
     else raise TEST lthy3
 
-  val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
-  val bns = raw_bn_funs ~~ bn_nos;
-
   val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = 
     if get_STEPS lthy3a > 3 
     then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a
     else raise TEST lthy3a
 
   (* definition of raw alphas *)
+  val _ = warning "Definition of alphas";
   val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
     if get_STEPS lthy3b > 4 
     then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b
     else raise TEST lthy3b
   
   (* definition of alpha-distinct lemmas *)
+  val _ = warning "Distinct theorems";
   val (alpha_distincts, alpha_bn_distincts) = 
     mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info
 
   (* definition of raw_alpha_eq_iff  lemmas *)
+  val _ = warning "Eq-iff theorems";
   val alpha_eq_iff = 
     if get_STEPS lthy > 5
     then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases
@@ -418,13 +420,18 @@
   (* proving alpha equivalence *)
   val _ = warning "Proving equivalence"
 
+  val alpha_refl_thms = 
+    if get_STEPS lthy > 9
+    then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy_tmp'' 
+    else raise TEST lthy4
+
   val alpha_sym_thms = 
-    if get_STEPS lthy > 9
+    if get_STEPS lthy > 10
     then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy_tmp'' 
     else raise TEST lthy4
 
   val alpha_trans_thms = 
-    if get_STEPS lthy > 10
+    if get_STEPS lthy > 11
     then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) 
            alpha_intros alpha_induct alpha_cases lthy_tmp'' 
     else raise TEST lthy4
@@ -432,13 +439,16 @@
 
   val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms))
   val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms))
-  val _ = tracing ("alpha_trans\n" ^ 
-    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_trans_thms))
+  val _ = tracing ("alpha_refl\n" ^ 
+    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms))
 
   val _ = 
-    if get_STEPS lthy > 11
+    if get_STEPS lthy > 12
     then true else raise TEST lthy4
 
+  val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
+  val bns = raw_bn_funs ~~ bn_nos;
+
   val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
 
   val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4;
diff -r 4e5a7b606eab -r 08bbde090a17 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Thu Jun 10 14:53:45 2010 +0200
+++ b/Nominal/nominal_dt_alpha.ML	Fri Jun 11 03:02:42 2010 +0200
@@ -16,6 +16,7 @@
 
   val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list
 
+  val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list
   val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list
   val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list
 end
@@ -246,6 +247,7 @@
 end
 
 
+
 (** produces the distinctness theorems **)
 
 (* transforms the distinctness theorems of the constructors 
@@ -289,9 +291,9 @@
 end
 
 
+
 (** produces the alpha_eq_iff simplification rules **)
 
-
 (* in case a theorem is of the form (C.. = C..), it will be
    rewritten to ((C.. = C..) = True) *)
 fun mk_simp_rule thm =
@@ -329,6 +331,56 @@
 
 
 
+(** reflexivity proof for the alphas **)
+
+val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}
+
+fun cases_tac intros =
+let
+  val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps}
+
+  val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac  
+
+  val bound_tac = 
+    EVERY' [ rtac exi_zero, 
+             resolve_tac @{thms alpha_gen_refl}, 
+             asm_full_simp_tac (HOL_ss addsimps prod_simps) ]
+in
+  REPEAT o FIRST' [rtac @{thm conjI}, 
+    resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]]
+end
+
+fun raw_prove_refl alpha_trms alpha_bns alpha_intros raw_dt_induct ctxt =
+let
+  val arg_tys = 
+    alpha_trms
+    |> map fastype_of
+    |> map domain_type
+  val arg_bn_tys = 
+    alpha_bns
+    |> map fastype_of
+    |> map domain_type
+  val arg_names = Datatype_Prop.make_tnames arg_tys
+  val arg_bn_names = map (fn ty => the (AList.lookup (op=) (arg_tys ~~ arg_names) ty)) arg_bn_tys
+  val args = map Free (arg_names ~~ arg_tys)
+  val arg_bns = map Free (arg_bn_names ~~ arg_bn_tys)
+  val goal = 
+    AList.group (op=) ((arg_bns ~~ alpha_bns) @ (args ~~ alpha_trms))
+    |> map (fn (ar, cnsts) => map (fn c => c $ ar $ ar) cnsts) 
+    |> map (foldr1 HOLogic.mk_conj)
+    |> foldr1 HOLogic.mk_conj
+    |> HOLogic.mk_Trueprop
+in
+  Goal.prove ctxt arg_names [] goal
+    (fn {context, ...} => 
+       HEADGOAL (DETERM o (rtac raw_dt_induct) THEN_ALL_NEW cases_tac alpha_intros)) 
+  |> Datatype_Aux.split_conj_thm 
+  |> map Datatype_Aux.split_conj_thm 
+  |> flat
+end
+
+
+
 (** symmetry proof for the alphas **)
 
 val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p"