# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1284990765 -28800
# Node ID ac7dff1194e89a099f3156be9f469e4082c1905a
# Parent  a9b6a00b1ba06a6ace62bb25b1edc99c5530d0b1
introduced a general procedure for structural inductions; simplified reflexivity proof

diff -r a9b6a00b1ba0 -r ac7dff1194e8 IsaMakefile
--- a/IsaMakefile	Sat Sep 18 06:09:43 2010 +0800
+++ b/IsaMakefile	Mon Sep 20 21:52:45 2010 +0800
@@ -20,8 +20,8 @@
 
 tests: $(LOG)/HOL-Nominal2.gz
 
-#$(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy
-#	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal
+$(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy
+	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal
 
 ## Nominal2 Paper
 
diff -r a9b6a00b1ba0 -r ac7dff1194e8 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Sat Sep 18 06:09:43 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Mon Sep 20 21:52:45 2010 +0800
@@ -6,6 +6,8 @@
 
 signature NOMINAL_LIBRARY =
 sig
+  val is_true: term -> bool
+
   val last2: 'a list -> 'a * 'a
 
   val dest_listT: typ -> typ
@@ -87,6 +89,9 @@
 structure Nominal_Library: NOMINAL_LIBRARY =
 struct
 
+fun is_true @{term "Trueprop True"} = true
+  | is_true _ = false 
+
 fun last2 [] = raise Empty
   | last2 [_] = raise Empty
   | last2 [x, y] = (x, y)
@@ -256,7 +261,7 @@
         SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT)
       | mk_size_measure T = size_const T
 
-    val ((_ $ (_ $ rel)) :: tl) = prems_of st
+    val ((_ $ (_ $ rel)) :: _) = prems_of st
     val measure_trm = 
       fastype_of rel 
       |> HOLogic.dest_setT
@@ -324,7 +329,7 @@
  R ... /\ P ...; split_conj_i picks out
  the part R or P part
 *)
-fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ f2) = 
+fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) = 
   (case head_of f1 of
      Const (name, _) => if member (op =) names name then SOME f1 else NONE
    | _ => NONE)
diff -r a9b6a00b1ba0 -r ac7dff1194e8 Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Sat Sep 18 06:09:43 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy	Mon Sep 20 21:52:45 2010 +0800
@@ -8,7 +8,7 @@
 atom_decl cvar
 atom_decl tvar
 
-declare [[STEPS = 100]]
+declare [[STEPS = 31]]
 
 nominal_datatype core_haskell: 
  tkind =
diff -r a9b6a00b1ba0 -r ac7dff1194e8 Nominal/Ex/ExPS7.thy
--- a/Nominal/Ex/ExPS7.thy	Sat Sep 18 06:09:43 2010 +0800
+++ b/Nominal/Ex/ExPS7.thy	Mon Sep 20 21:52:45 2010 +0800
@@ -6,6 +6,8 @@
 
 atom_decl name
 
+declare [[STEPS = 31]]
+
 nominal_datatype exp =
   Var name
 | Unit
diff -r a9b6a00b1ba0 -r ac7dff1194e8 Nominal/Ex/Modules.thy
--- a/Nominal/Ex/Modules.thy	Sat Sep 18 06:09:43 2010 +0800
+++ b/Nominal/Ex/Modules.thy	Mon Sep 20 21:52:45 2010 +0800
@@ -7,6 +7,9 @@
 
 atom_decl name
 
+declare [[STEPS = 31]]
+
+
 nominal_datatype modules: 
  mexp =
   Acc "path"
diff -r a9b6a00b1ba0 -r ac7dff1194e8 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Sat Sep 18 06:09:43 2010 +0800
+++ b/Nominal/Ex/TypeSchemes.thy	Mon Sep 20 21:52:45 2010 +0800
@@ -46,6 +46,7 @@
 thm tys2.fsupp
 
 
+
 text {* *}
 
 (*
diff -r a9b6a00b1ba0 -r ac7dff1194e8 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Sat Sep 18 06:09:43 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Mon Sep 20 21:52:45 2010 +0800
@@ -16,6 +16,9 @@
   val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
     thm list -> thm list
 
+  val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> 
+    (Proof.context -> int -> tactic) -> Proof.context -> thm list
+  
   val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> 
     (Proof.context -> int -> tactic) -> Proof.context -> thm list
 
@@ -351,10 +354,44 @@
   end
 
 
-(** proof by induction over the alpha-definitions **)
+(** proof by induction over types **)
+
+fun induct_prove tys props induct_thm cases_tac ctxt =
+  let
+    val (arg_names, ctxt') =
+      Variable.variant_fixes (replicate (length tys) "x") ctxt
+
+    val args = map2 (curry Free) arg_names tys
 
-fun is_true @{term "Trueprop True"} = true
-  | is_true _ = false 
+    val true_trms = replicate (length tys) (K @{term True})
+  
+    fun apply_all x fs = map (fn f => f x) fs
+    
+    val goals = 
+        group (props @ (tys ~~ true_trms))
+        |> map snd 
+        |> map2 apply_all args
+        |> map fold_conj
+        |> foldr1 HOLogic.mk_conj
+        |> HOLogic.mk_Trueprop
+
+    fun tac ctxt =
+      HEADGOAL 
+        (DETERM o (rtac induct_thm) 
+         THEN_ALL_NEW 
+           (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt])))
+  in
+    Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
+    |> singleton (ProofContext.export ctxt' ctxt)
+    |> Datatype_Aux.split_conj_thm
+    |> map Datatype_Aux.split_conj_thm
+    |> flat
+    |> filter_out (is_true o concl_of)
+    |> map zero_var_indexes
+  end
+
+
+(** proof by induction over the alpha-definitions **)
 
 fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt =
   let
@@ -397,8 +434,8 @@
     |> map (fn th => th RS mp) 
     |> map Datatype_Aux.split_conj_thm
     |> flat
+    |> filter_out (is_true o concl_of)
     |> map zero_var_indexes
-    |> filter_out (is_true o concl_of)
   end
 
 
@@ -406,7 +443,7 @@
 
 val exi_zero = @{lemma "P (0::perm) ==> (? x. P x)" by auto}
 
-fun cases_tac intros =
+fun cases_tac intros ctxt =
   let
     val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps}
 
@@ -417,8 +454,7 @@
                resolve_tac @{thms alpha_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]]
+    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 =
@@ -427,27 +463,17 @@
       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 (lookup (arg_tys ~~ arg_names)) arg_bn_tys
-    val args = map Free (arg_names ~~ arg_tys)
-    val arg_bns = map Free (arg_bn_names ~~ arg_bn_tys)
-    val goal = 
-      group ((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
+    
+    val props = 
+      map (fn (ty, c) => (ty, fn x => c $ x $ x)) 
+        ((arg_tys ~~ alpha_trms) @ (arg_bn_tys ~~ alpha_bns))
   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
+    induct_prove arg_tys props raw_dt_induct (cases_tac alpha_intros) ctxt 
   end