src/HOL/Nominal/nominal_induct.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/nominal_induct.ML	Mon Oct 17 12:30:57 2005 +0200
@@ -0,0 +1,88 @@
+(* $Id$ *)
+
+local
+
+(* A function that takes a list of Variables and a term t;                    *)
+(* it builds up an abstraction of the Variables packaged in a tuple(!)        *)
+(* over the term t.                                                           *)
+(* E.g  tuple_lambda [] t        produces %x . t where x is a dummy Variable  *) 
+(*      tuple_lambda [a] t       produces %a . t                              *) 
+(*      tuple_lambda [a,b,c] t   produces %(a,b,c). t                         *)
+
+  fun tuple_lambda [] t  = Abs ("x", HOLogic.unitT, t)
+    | tuple_lambda [x] t = lambda x t
+    | tuple_lambda (x::xs) t =
+       let
+         val t' = tuple_lambda xs t;
+         val Type ("fun", [T,U]) = fastype_of t';
+       in
+         HOLogic.split_const (fastype_of x,T,U) $ lambda x t'
+       end; 
+
+fun find_var frees name =
+  (case Library.find_first (equal name o fst o dest_Free) frees of
+    NONE => error ("No such Variable in term: " ^ quote name)
+  | SOME v => v);
+
+fun nominal_induct_tac (names, rule) facts state =
+  let
+    val sg     = Thm.sign_of_thm state;
+    val cert   = Thm.cterm_of sg;
+    val goal :: _ = Thm.prems_of state;  (*exception Subscript*)
+    val frees  = Term.term_frees goal;
+    val frees' = filter_out (fn Free (x, _) => exists (equal x) names) frees;
+    val vars = map (find_var frees) names;
+
+    fun inst_rule rule =
+      let
+        val concl_vars = map Var (rev (Term.add_vars (Thm.concl_of rule) []));
+        val (P :: ts, x) = split_last concl_vars
+          handle Empty => error "Malformed conclusion of induction rule"
+            | Bind => error "Malformed conclusion of induction rule";
+      in
+        cterm_instantiate
+          ((cert P, cert (fold_rev lambda vars (tuple_lambda frees' (HOLogic.dest_Trueprop goal)))) ::
+           (cert x, cert (if null frees' then HOLogic.unit else foldr1 HOLogic.mk_prod frees')) ::
+           (map cert ts ~~ map cert vars)) rule
+      end;
+
+    val simplify_rule =
+      Simplifier.full_simplify (HOL_basic_ss addsimps
+        [split_conv, split_paired_All, split_paired_all]);
+
+    val facts1 = Library.take (1, facts);
+    val facts2 = Library.drop (1, facts);
+
+  in
+    rule
+    |> inst_rule
+    |> Method.multi_resolve facts1
+    |> Seq.map simplify_rule
+    |> Seq.map (RuleCases.save rule)
+    |> Seq.map RuleCases.add
+    |> Seq.map (fn (r, (cases, _)) =>
+        HEADGOAL (Method.insert_tac facts2 THEN' Tactic.rtac r) state
+        |> Seq.map (rpair (RuleCases.make false NONE (sg, Thm.prop_of r) cases)))
+    |> Seq.flat
+  end
+  handle Subscript => Seq.empty;
+
+val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm;
+
+val nominal_induct_args =
+  Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name)) -- rule_spec;
+
+in
+
+val nominal_induct_method =
+  Method.RAW_METHOD_CASES o nominal_induct_tac oo (#2 oo Method.syntax nominal_induct_args);
+
+(* nominal_induc_method needs to have the type
+
+   Args.src -> Proof.context -> Proof.method
+
+   CHECK THAT
+
+*)
+
+end;