# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1293381316 0
# Node ID 16ffbc8442ca63d753c24145fe132b4d8f4ef833
# Parent  8a4c44cef353fae55a803c6bde50b70618551dbb
generated goals for strong induction theorems.

diff -r 8a4c44cef353 -r 16ffbc8442ca Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Thu Dec 23 01:05:05 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Sun Dec 26 16:35:16 2010 +0000
@@ -24,13 +24,15 @@
   "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
+
+
+
 thm foo.bn_defs
 thm foo.permute_bn
 thm foo.perm_bn_alpha
 thm foo.perm_bn_simps
 thm foo.bn_finite
 
-
 thm foo.distinct
 thm foo.induct
 thm foo.inducts
diff -r 8a4c44cef353 -r 16ffbc8442ca Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Thu Dec 23 01:05:05 2010 +0000
+++ b/Nominal/Nominal2.thy	Sun Dec 26 16:35:16 2010 +0000
@@ -529,9 +529,12 @@
     then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
     else []
 
+  (* proving the strong exhausts and induct lemmas *)
   val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs'
     qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms
 
+  val qstrong_induct_thm = prove_strong_induct lthyC qinduct qexhausts bclauses
+
 
   (* noting the theorems *)  
 
diff -r 8a4c44cef353 -r 16ffbc8442ca Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Thu Dec 23 01:05:05 2010 +0000
+++ b/Nominal/nominal_dt_quot.ML	Sun Dec 26 16:35:16 2010 +0000
@@ -42,6 +42,7 @@
   val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list -> 
     thm list -> thm list -> thm list -> thm list -> thm list
 
+  val prove_strong_induct: Proof.context -> thm -> thm list -> bclause list list list -> thm
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -608,5 +609,96 @@
     |> ProofContext.export lthy'' lthy
   end
 
+
+
+(** strong induction theorems **)
+
+fun add_c_prop c c_ty trm =
+  let
+    val (P, arg) = dest_comb trm
+    val (P_name, P_ty) = dest_Free P
+    val (ty_args, bool) = strip_type P_ty
+  in
+    Free (P_name, (c_ty :: ty_args) ---> bool) $ c $ arg
+  end
+
+fun add_qnt_c_prop c_name c_ty trm =
+  trm |> HOLogic.dest_Trueprop
+      |> incr_boundvars 1
+      |> add_c_prop (Bound 0) c_ty
+      |> HOLogic.mk_Trueprop 
+      |> mk_all (c_name, c_ty)
+
+fun prep_prem lthy c (c_name, c_ty) bclauses (params, prems, concl) =
+  let
+    val tys = map snd params
+    val binders = get_all_binders bclauses
+   
+    fun prep_binder (opt, i) = 
+      let
+        val t = Bound (length tys - i - 1)
+      in
+        case opt of
+          NONE => setify_ty lthy (nth tys i) t 
+        | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t)   
+      end 
+
+    val prems' = prems
+      |> map (incr_boundvars 1) 
+      |> map (add_qnt_c_prop c_name c_ty)
+
+    val prems'' = 
+      case binders of
+        [] => prems'                       (* case: no binders *)
+      | _ => binders                       (* case: binders *) 
+          |> map prep_binder
+          |> fold_union_env tys
+          |> incr_boundvars 1
+          |> (fn t => mk_fresh_star_ty c_ty t (Bound 0))
+          |> (fn t => HOLogic.mk_Trueprop t :: prems')
+
+    val concl' = concl
+      |> HOLogic.dest_Trueprop
+      |> incr_boundvars 1 
+      |> add_c_prop (Bound 0) c_ty  
+      |> HOLogic.mk_Trueprop
+  in  
+    mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl'
+  end
+
+fun prove_strong_induct lthy induct exhausts bclausesss =
+  let
+    val ((insts, [induct']), lthy') = Variable.import true [induct] lthy
+
+    val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
+    val c_ty = TFree (a, @{sort fs})
+    val c = Free (c_name, c_ty)
+
+    val (prems, concl) = induct'
+      |> prop_of
+      |> Logic.strip_horn 
+
+    val concls = concl
+      |> HOLogic.dest_Trueprop
+      |> HOLogic.dest_conj 
+      |> map (add_c_prop c c_ty) 
+      |> map HOLogic.mk_Trueprop
+
+    val prems' = prems
+      |> map strip_full_horn
+      |> map2 (prep_prem lthy'' c (c_name, c_ty)) (flat bclausesss)
+      |> map (Syntax.check_term lthy'') 
+
+    val _ = tracing ("induct:\n" ^ Syntax.string_of_term lthy'' (prop_of induct'))
+    val _ = tracing ("concls:\n" ^ commas (map (Syntax.string_of_term lthy'') concls))  
+    val _ = tracing ("prems':\n" ^ cat_lines (map (Syntax.string_of_term lthy'') prems'))
+
+    val thm = Goal.prove_multi lthy'' [] prems' concls
+      (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy''))
+  in
+    @{thm TrueI}
+  end
+
+
 end (* structure *)