--- a/Nominal/nominal_inductive.ML Tue Mar 26 16:41:31 2013 +0100
+++ b/Nominal/nominal_inductive.ML Wed Mar 27 16:08:30 2013 +0100
@@ -1,5 +1,6 @@
(* Title: nominal_inductive.ML
Author: Christian Urban
+ Author: Tjark Weber
Infrastructure for proving strong induction theorems
for inductive predicates involving nominal datatypes.
@@ -7,27 +8,26 @@
Code based on an earlier version by Stefan Berghofer.
*)
-
signature NOMINAL_INDUCTIVE =
sig
- val prove_strong_inductive: string list -> string list -> term list list -> thm -> thm list ->
+ val prove_strong_inductive: string list -> string list -> term list list -> thm -> thm list ->
Proof.context -> Proof.state
-
val prove_strong_inductive_cmd: xstring * (string * string list) list -> Proof.context -> Proof.state
end
structure Nominal_Inductive : NOMINAL_INDUCTIVE =
struct
-
-fun mk_cplus p q = Thm.apply (Thm.apply @{cterm "plus :: perm => perm => perm"} p) q
+fun mk_cplus p q =
+ Thm.apply (Thm.apply @{cterm "plus :: perm => perm => perm"} p) q
-fun mk_cminus p = Thm.apply @{cterm "uminus :: perm => perm"} p
+fun mk_cminus p =
+ Thm.apply @{cterm "uminus :: perm => perm"} p
-fun minus_permute_intro_tac p =
+fun minus_permute_intro_tac p =
rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE})
-fun minus_permute_elim p thm =
+fun minus_permute_elim p thm =
thm RS (Drule.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI})
(* fixme: move to nominal_library *)
@@ -36,25 +36,28 @@
| real_head_of (Const (@{const_name all}, _) $ Abs (_, _, t)) = real_head_of t
| real_head_of (Const (@{const_name All}, _) $ Abs (_, _, t)) = real_head_of t
| real_head_of (Const ("HOL.induct_forall", _) $ Abs (_, _, t)) = real_head_of t
- | real_head_of t = head_of t
+ | real_head_of t = head_of t
-fun mk_vc_compat (avoid, avoid_trm) prems concl_args params =
- let
- val vc_goal = concl_args
- |> HOLogic.mk_tuple
- |> mk_fresh_star avoid_trm
- |> HOLogic.mk_Trueprop
- |> (curry Logic.list_implies) prems
- |> fold_rev (Logic.all o Free) params
- val finite_goal = avoid_trm
- |> mk_finite
- |> HOLogic.mk_Trueprop
- |> (curry Logic.list_implies) prems
- |> fold_rev (Logic.all o Free) params
- in
- if null avoid then [] else [vc_goal, finite_goal]
- end
+fun mk_vc_compat (avoid, avoid_trm) prems concl_args params =
+ if null avoid then
+ []
+ else
+ let
+ val vc_goal = concl_args
+ |> HOLogic.mk_tuple
+ |> mk_fresh_star avoid_trm
+ |> HOLogic.mk_Trueprop
+ |> (curry Logic.list_implies) prems
+ |> fold_rev (Logic.all o Free) params
+ val finite_goal = avoid_trm
+ |> mk_finite
+ |> HOLogic.mk_Trueprop
+ |> (curry Logic.list_implies) prems
+ |> fold_rev (Logic.all o Free) params
+ in
+ [vc_goal, finite_goal]
+ end
(* fixme: move to nominal_library *)
fun map_term prop f trm =
@@ -77,12 +80,15 @@
|> (fn t => HOLogic.all_const @{typ perm} $ lambda p t)
end
-fun induct_forall_const T = Const ("HOL.induct_forall", (T --> @{typ bool}) --> @{typ bool})
-fun mk_induct_forall (a, T) t = induct_forall_const T $ Abs (a, T, t)
+fun induct_forall_const T =
+ Const ("HOL.induct_forall", (T --> @{typ bool}) --> @{typ bool})
+
+fun mk_induct_forall (a, T) t =
+ induct_forall_const T $ Abs (a, T, t)
fun add_c_prop qnt Ps (c, c_name, c_ty) trm =
let
- fun add t =
+ fun add t =
let
val (P, args) = strip_comb t
val (P_name, P_ty) = dest_Free P
@@ -91,7 +97,7 @@
|> qnt ? map (incr_boundvars 1)
in
list_comb (Free (P_name, (c_ty :: ty_args) ---> bool), c :: args')
- |> qnt ? mk_induct_forall (c_name, c_ty)
+ |> qnt ? mk_induct_forall (c_name, c_ty)
end
in
map_term (member (op =) Ps o head_of) add trm
@@ -100,7 +106,7 @@
fun prep_prem Ps c_name c_ty (avoid, avoid_trm) (params, prems, concl) =
let
val prems' = prems
- |> map (incr_boundvars 1)
+ |> map (incr_boundvars 1)
|> map (add_c_prop true Ps (Bound 0, c_name, c_ty))
val avoid_trm' = avoid_trm
@@ -109,14 +115,14 @@
|> (fn t => mk_fresh_star_ty c_ty t (Bound 0))
|> HOLogic.mk_Trueprop
- val prems'' =
- if null avoid
- then prems'
+ val prems'' =
+ if null avoid
+ then prems'
else avoid_trm' :: prems'
val concl' = concl
- |> incr_boundvars 1
- |> add_c_prop false Ps (Bound 0, c_name, c_ty)
+ |> incr_boundvars 1
+ |> add_c_prop false Ps (Bound 0, c_name, c_ty)
in
mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl'
end
@@ -129,7 +135,7 @@
(* fixme: move to nominal_library *)
fun map7 _ [] [] [] [] [] [] [] = []
- | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (r :: rs) (s :: ss) =
+ | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (r :: rs) (s :: ss) =
f x y z u v r s :: map7 f xs ys zs us vs rs ss
(* local abbreviations *)
@@ -137,18 +143,20 @@
local
open Nominal_Permeq
in
-(* by default eqvt_strict_config contains unwanted @{thm permute_pure} *)
+
+ (* by default eqvt_strict_config contains unwanted @{thm permute_pure} *)
-val eqvt_sconfig = eqvt_strict_config addpres @{thms permute_minus_cancel}
+ val eqvt_sconfig = eqvt_strict_config addpres @{thms permute_minus_cancel}
-fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig
-fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig
+ fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig
+ fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig
end
val all_elims =
let
- fun spec' ct = Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}
+ fun spec' ct =
+ Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}
in
fold (fn ct => fn th => th RS spec' ct)
end
@@ -216,6 +224,7 @@
val supp_perm_eq' = @{lemma "fresh_star (supp (permute p x)) q ==> permute p x == permute (q + p) x"
by (simp add: supp_perm_eq)}
+
val fresh_star_plus = @{lemma "fresh_star (permute q (permute p x)) c ==> fresh_star (permute (q + p) x) c"
by (simp add: permute_plus)}
@@ -321,8 +330,9 @@
|> map Logic.strip_horn
|> split_list
- val intr_concls_args = map (snd o strip_comb o HOLogic.dest_Trueprop) intr_concls
-
+ val intr_concls_args =
+ map (snd o fixed_nonfixed_args ctxt' o HOLogic.dest_Trueprop) intr_concls
+
val avoid_trms = avoids
|> (map o map) (setify ctxt')
|> map fold_union
@@ -383,35 +393,33 @@
fun prove_strong_inductive_cmd (pred_name, avoids) ctxt =
let
- val thy = Proof_Context.theory_of ctxt;
val ({names, ...}, {raw_induct, intrs, ...}) =
- Inductive.the_inductive ctxt (Sign.intern_const thy pred_name);
+ Inductive.the_inductive ctxt (long_name ctxt pred_name)
- val rule_names =
- hd names
+ val rule_names = hd names
|> the o Induct.lookup_inductP ctxt
|> fst o Rule_Cases.get
|> map (fst o fst)
- val _ = (case duplicates (op = o pairself fst) avoids of
+ val case_names = map fst avoids
+ val _ = case duplicates (op =) case_names of
[] => ()
- | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)))
-
- val _ = (case subtract (op =) rule_names (map fst avoids) of
+ | xs => error ("Duplicate case names: " ^ commas_quote xs)
+ val _ = case subtract (op =) rule_names case_names of
[] => ()
- | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs))
+ | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs)
val avoids_ordered = order_default (op =) [] rule_names avoids
-
+
fun read_avoids avoid_trms intr =
let
(* fixme hack *)
val (((_, ctrms), _), ctxt') = Variable.import true [intr] ctxt
val trms = map (term_of o snd) ctrms
- val ctxt'' = fold Variable.declare_term trms ctxt'
+ val ctxt'' = fold Variable.declare_term trms ctxt'
in
- map (Syntax.read_term ctxt'') avoid_trms
- end
+ map (Syntax.read_term ctxt'') avoid_trms
+ end
val avoid_trms = map2 read_avoids avoids_ordered intrs
in
@@ -420,11 +428,10 @@
(* outer syntax *)
local
-
- val single_avoid_parser =
+ val single_avoid_parser =
Parse.name -- (@{keyword ":"} |-- Parse.and_list1 Parse.term)
- val avoids_parser =
+ val avoids_parser =
Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) []
val main_parser = Parse.xname -- avoids_parser