# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1280535879 -3600
# Node ID 0f24c961b5f69b0ca7c2267718c442f561413797
# Parent  ebf253d806708b84af70fd0541520af0305b66bf
introduced a general alpha_prove method

diff -r ebf253d80670 -r 0f24c961b5f6 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Fri Jul 30 00:40:32 2010 +0100
+++ b/Nominal-General/nominal_library.ML	Sat Jul 31 01:24:39 2010 +0100
@@ -35,6 +35,8 @@
   val mk_append: term * term -> term
   val mk_union: term * term -> term
   val fold_union: term list -> term
+  val mk_conj: term * term -> term
+  val fold_conj: term list -> term
 
   (* datatype operations *)
   val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
@@ -102,20 +104,21 @@
   | mk_diff (t1, @{term "{}::atom set"}) = t1
   | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
 
-fun mk_append (@{term "[]::atom list"}, @{term "[]::atom list"}) = @{term "[]::atom list"}
-  | mk_append (t1, @{term "[]::atom list"}) = t1
+fun mk_append (t1, @{term "[]::atom list"}) = t1
   | mk_append (@{term "[]::atom list"}, t2) = t2
   | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) 
 
-fun mk_union (@{term "{}::atom set"}, @{term "{}::atom set"}) = @{term "{}::atom set"}
-  | mk_union (t1 , @{term "{}::atom set"}) = t1
+fun mk_union (t1, @{term "{}::atom set"}) = t1
   | mk_union (@{term "{}::atom set"}, t2) = t2
   | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2)  
  
 fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"}
 
+fun mk_conj (t1, @{term "True"}) = t1
+  | mk_conj (@{term "True"}, t2) = t2
+  | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2)
 
-
+fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}
 
 (** datatypes **)
 
diff -r ebf253d80670 -r 0f24c961b5f6 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Fri Jul 30 00:40:32 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Sat Jul 31 01:24:39 2010 +0100
@@ -21,6 +21,8 @@
 where
   "bn (As x y t) = {atom x}"
 
+thm alpha_sym_thms
+thm alpha_trans_thms
 thm size_eqvt
 thm alpha_bn_imps
 thm distinct
diff -r ebf253d80670 -r 0f24c961b5f6 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Fri Jul 30 00:40:32 2010 +0100
+++ b/Nominal/NewParser.thy	Sat Jul 31 01:24:39 2010 +0100
@@ -391,10 +391,12 @@
       (Local_Theory.restore lthy_tmp)
     else raise TEST lthy4
 
-  val size_eqvt = 
+  val raw_size_eqvt = 
     if get_STEPS lthy > 8
     then raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) 
       (Local_Theory.restore lthy_tmp)
+      |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]})
+      |> map (fn thm => thm RS @{thm sym})
     else raise TEST lthy4
  
   val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
@@ -501,7 +503,9 @@
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
      ||>> 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"}, []), size_eqvt)
+     ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt)
+     ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms)
+     ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms)
   
   val _ = 
     if get_STEPS lthy > 17
diff -r ebf253d80670 -r 0f24c961b5f6 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Fri Jul 30 00:40:32 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Sat Jul 31 01:24:39 2010 +0100
@@ -17,6 +17,9 @@
   val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
     thm list -> (thm list * thm list)
 
+  val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> 
+    (Proof.context -> int -> tactic) -> Proof.context -> 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
@@ -340,6 +343,52 @@
 end
 
 
+(** proof by induction over the alpha-definitions **)
+
+fun is_true @{term "Trueprop True"} = true
+  | is_true _ = false 
+
+fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt =
+let
+  val arg_tys = map (domain_type o fastype_of) alphas
+
+  val ((arg_names1, arg_names2), ctxt') =
+    ctxt
+    |> Variable.variant_fixes (replicate (length alphas) "x") 
+    ||>> Variable.variant_fixes (replicate (length alphas) "y")
+
+  val args1 = map2 (curry Free) arg_names1 arg_tys
+  val args2 = map2 (curry Free) arg_names2 arg_tys
+
+  val true_trms = replicate (length alphas) (K @{term True})
+  
+  fun apply_all x fs = map (fn f => f x) fs
+  val goal_rhs = 
+    group (props @ (alphas ~~ true_trms))
+    |> map snd 
+    |> map2 apply_all (args1 ~~ args2)
+    |> map fold_conj
+
+  fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2
+  val goal_lhs = map2 apply_trm_pair alphas (args1 ~~ args2)
+
+  val goal =
+    (map2 (curry HOLogic.mk_imp) goal_lhs goal_rhs)
+    |> foldr1 HOLogic.mk_conj
+    |> HOLogic.mk_Trueprop
+in
+  Goal.prove ctxt' [] [] goal
+    (fn {context, ...} => HEADGOAL 
+      (DETERM o (rtac alpha_induct_thm) THEN_ALL_NEW (rtac @{thm TrueI} ORELSE' cases_tac context)))
+  |> singleton (ProofContext.export ctxt' ctxt)
+  |> Datatype_Aux.split_conj_thm 
+  |> map Datatype_Aux.split_conj_thm
+  |> flat
+  |> map zero_var_indexes
+  |> map (fn th => th RS mp)
+  |> filter_out (is_true o concl_of)
+end
+
 
 (** reflexivity proof for the alphas **)
 
@@ -416,51 +465,22 @@
       trans_prem_tac pred_names ctxt ] 
 end
 
-fun prove_sym_tac pred_names intros induct ctxt =
-let
-  val prem_eq_tac = rtac @{thm sym} THEN' atac   
-  val prem_unbound_tac = atac
-
-  val prem_cases_tacs = FIRST' 
-    [prem_eq_tac, prem_unbound_tac, prem_bound_tac pred_names ctxt]
-in
-  HEADGOAL (rtac induct THEN_ALL_NEW 
-    (resolve_tac intros THEN_ALL_NEW prem_cases_tacs))
-end
-
-fun prep_sym_goal alpha_trm (arg1, arg2) =
-let
-  val lhs = alpha_trm $ arg1 $ arg2
-  val rhs = alpha_trm $ arg2 $ arg1
-in
-  HOLogic.mk_imp (lhs, rhs)  
-end
-
 fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt =
 let
-  val alpha_names =  map (fst o dest_Const) alpha_trms
-  val arg_tys = 
-    alpha_trms
-    |> map fastype_of
-    |> map domain_type  
-  val (arg_names1, (arg_names2, ctxt')) =
-    ctxt
-    |> Variable.variant_fixes (replicate (length arg_tys) "x") 
-    ||> Variable.variant_fixes (replicate (length arg_tys) "y")   
-  val args1 = map Free (arg_names1 ~~ arg_tys) 
-  val args2 = map Free (arg_names2 ~~ arg_tys)
-  val goal = HOLogic.mk_Trueprop 
-    (foldr1 HOLogic.mk_conj (map2 prep_sym_goal alpha_trms (args1 ~~ args2)))	      
+  val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms
+  
+  fun tac ctxt = 
+    let
+      val alpha_names =  map (fst o dest_Const) alpha_trms   
+    in
+      resolve_tac alpha_intros THEN_ALL_NEW 
+      FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names ctxt]
+  end
 in
-  Goal.prove ctxt' [] [] goal 
-    (fn {context,...} =>  prove_sym_tac alpha_names alpha_intros alpha_induct context)
-    |> singleton (ProofContext.export ctxt' ctxt)
-    |> Datatype_Aux.split_conj_thm 
-    |> map (fn th => zero_var_indexes (th RS mp))
+  alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt 
 end
 
 
-
 (** transitivity proof for alphas **)
 
 (* applies cases rules and resolves them with the last premise *)
@@ -500,58 +520,39 @@
         asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
 end
 			  
-fun prove_trans_tac pred_names raw_dt_thms intros induct cases ctxt =
+fun prove_trans_tac pred_names raw_dt_thms intros cases ctxt =
 let
   fun all_cases ctxt = 
     asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) 
     THEN' TRY o non_trivial_cases_tac pred_names intros ctxt
 in
-  HEADGOAL (rtac induct THEN_ALL_NEW  
-    EVERY' [ rtac @{thm allI}, rtac @{thm impI}, 
-             ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ])
+  EVERY' [ rtac @{thm allI}, rtac @{thm impI}, 
+           ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ]
 end
 
-fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) =
+fun prep_trans_goal alpha_trm (arg1, arg2) =
 let
-  val lhs = alpha_trm $ arg1 $ arg2
+  val arg_ty = fastype_of arg1
   val mid = alpha_trm $ arg2 $ (Bound 0)
   val rhs = alpha_trm $ arg1 $ (Bound 0) 
 in
-  HOLogic.mk_imp (lhs, 
-    HOLogic.all_const arg_ty $ Abs ("z", arg_ty, 
-      HOLogic.mk_imp (mid, rhs)))
+  HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs))
 end
 
-val norm = @{lemma "A --> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp}
-
 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt =
 let
-  val alpha_names =  map (fst o dest_Const) alpha_trms
-  val arg_tys = 
-    alpha_trms
-    |> map fastype_of
-    |> map domain_type  
-  val (arg_names1, (arg_names2, ctxt')) =
-    ctxt
-    |> Variable.variant_fixes (replicate (length arg_tys) "x") 
-    ||> Variable.variant_fixes (replicate (length arg_tys) "y")
-  val args1 = map Free (arg_names1 ~~ arg_tys) 
-  val args2 = map Free (arg_names2 ~~ arg_tys)
-  val goal = HOLogic.mk_Trueprop 
-    (foldr1 HOLogic.mk_conj (map2 prep_trans_goal alpha_trms (args1 ~~ args2 ~~ arg_tys))) 
+  val alpha_names =  map (fst o dest_Const) alpha_trms 
+  val props = map prep_trans_goal alpha_trms
+  val norm = @{lemma "A ==> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp}  
 in
-  Goal.prove ctxt' [] [] goal 
-    (fn {context,...} =>  
-       prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_induct alpha_cases context)
-    |> singleton (ProofContext.export ctxt' ctxt)
-    |> Datatype_Aux.split_conj_thm 
-    |> map (fn th => zero_var_indexes (th RS norm))
+  alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct
+    (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt
 end
 
 (* proves the equivp predicate for all alphas *)
 
 val equivp_intro = 
-  @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y z. R x y --> R y z --> R x z|] ==> equivp R"
+  @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y. R x y --> (!z. R y z --> R x z)|] ==> equivp R"
     by (rule equivpI, unfold reflp_def symp_def transp_def, blast+)}
 
 fun raw_prove_equivp alphas refl symm trans ctxt = 
@@ -571,9 +572,6 @@
 
 (* proves that alpha_raw implies alpha_bn *)
 
-fun is_true @{term "Trueprop True"} = true
-  | is_true _ = false 
-
 fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = 
   SUBPROOF (fn {prems, context, ...} => 
     let