# HG changeset patch # User haftmann # Date 1324739698 -3600 # Node ID 296d9a9c8d24d63b24175573890229ba7cbc9e8e # Parent d3325de5f2999b37bbfffa7197507f5234951d69 treatment of type constructor `set` diff -r d3325de5f299 -r 296d9a9c8d24 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Sat Dec 24 15:55:03 2011 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Sat Dec 24 16:14:58 2011 +0100 @@ -494,6 +494,7 @@ val pt_optn_inst = @{thm "pt_option_inst"}; val pt_noptn_inst = @{thm "pt_noption_inst"}; val pt_fun_inst = @{thm "pt_fun_inst"}; + val pt_set_inst = @{thm "pt_set_inst"}; (* for all atom-kind combinations / show that *) (* every is an instance of pt_; the proof for *) @@ -541,6 +542,7 @@ rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1]; val pt_thm_fun = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst)); + val pt_thm_set = at_thm RS (pt_inst RS pt_set_inst); val pt_thm_noptn = pt_inst RS pt_noptn_inst; val pt_thm_optn = pt_inst RS pt_optn_inst; val pt_thm_list = pt_inst RS pt_list_inst; @@ -550,6 +552,7 @@ in thy |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun) + |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set) |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn) |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list) diff -r d3325de5f299 -r 296d9a9c8d24 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Sat Dec 24 15:55:03 2011 +0100 +++ b/src/HOL/Tools/inductive_set.ML Sat Dec 24 16:14:58 2011 +0100 @@ -244,7 +244,7 @@ NONE => thm' RS sym | SOME fs' => let - val U = List.last (binder_types T); + val U = HOLogic.dest_setT (body_type T); val Ts = HOLogic.strip_ptupleT fs' U; (* FIXME: should cterm_instantiate increment indexes? *) val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong; @@ -351,7 +351,7 @@ end; val to_pred_att = Thm.rule_attribute o to_pred; - + (**** convert theorem in predicate notation to set notation ****) @@ -421,7 +421,7 @@ | infer (t $ u) = infer t #> infer u | infer _ = I; val new_arities = filter_out - (fn (x as Free (_, T), _) => member (op =) params x andalso length (binder_types T) > 1 + (fn (x as Free (_, T), _) => member (op =) params x andalso length (binder_types T) > 0 | _ => false) (fold (snd #> infer) intros []); val params' = map (fn x => (case AList.lookup op = new_arities x of @@ -447,7 +447,7 @@ val ((cs', cs_info), eqns) = cs |> map (fn c as Free (s, T) => let val fs = the_default [] (AList.lookup op = new_arities c); - val (Us, U) = split_last (binder_types T); + val (Us, U) = strip_type T |> apsnd HOLogic.dest_setT; val _ = Us = paramTs orelse error (Pretty.string_of (Pretty.chunks [Pretty.str "Argument types", Pretty.block (Pretty.commas (map (Syntax.pretty_typ lthy) Us)),