# HG changeset patch # User berghofe # Date 1148457756 -7200 # Node ID ee9c7fa80d210683ad1e523e4bc71a630dc191dc # Parent 78cd5f6af8e8df9e2fdf0e02fcf9ba1d27a44fcd Extended strong induction rule with additional freshness constraints. diff -r 78cd5f6af8e8 -r ee9c7fa80d21 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Wed May 24 01:47:25 2006 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Wed May 24 10:02:36 2006 +0200 @@ -677,6 +677,9 @@ val (descr1, descr2) = chop (length new_type_names) descr''; val descr' = [descr1, descr2]; + fun partition_cargs idxs xs = map (fn (i, j) => + (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs; + val typ_of_dtyp' = replace_types' o typ_of_dtyp descr sorts'; val rep_names = map (fn s => @@ -1119,6 +1122,7 @@ val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames); val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs)); val frees = tnames ~~ Ts; + val frees' = partition_cargs idxs frees; val z = (variant tnames "z", fsT); fun mk_prem ((dt, s), T) = @@ -1129,11 +1133,24 @@ (make_pred fsT (body_index dt) U $ Bound l $ app_bnds (Free (s, T)) l)) end; + fun mk_fresh1 xs [] = [] + | mk_fresh1 xs ((y as (_, T)):: ys) = map (fn x => HOLogic.mk_Trueprop + (HOLogic.mk_not (HOLogic.mk_eq (Free y, Free x)))) + (filter (fn (_, U) => T = U) (rev xs)) @ + mk_fresh1 (y :: xs) ys; + + fun mk_fresh2 xss [] = [] + | mk_fresh2 xss ((p as (ys, _)) :: yss) = List.concat (map (fn y as (_, T) => + map (fn (_, x as (_, U)) => HOLogic.mk_Trueprop + (Const ("Nominal.fresh", T --> U --> HOLogic.boolT) $ Free y $ Free x)) + (rev xss @ yss)) ys) @ + mk_fresh2 (p :: xss) yss; + val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs'); val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop - (f T (Free p) (Free z))) - (map (curry List.nth frees) (List.concat (map (fn (m, n) => - m upto m + n - 1) idxs))) + (f T (Free p) (Free z))) (List.concat (map fst frees')) @ + mk_fresh1 [] (List.concat (map fst frees')) @ + mk_fresh2 [] frees' in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems, HOLogic.mk_Trueprop (make_pred fsT k T $ Free z $ @@ -1198,7 +1215,7 @@ Const ("List.list.Nil", pT) end; - fun mk_fresh i i' j k p l vs _ _ = + fun mk_fresh i i' j k p l is vs _ _ = let val n = length vs; val Ts = map snd vs; @@ -1206,18 +1223,25 @@ val f = the (AList.lookup op = fresh_fs T); val U = List.nth (Ts, n - i' - 1); val S = HOLogic.mk_setT T; + val prms' = map Bound (n - k downto n - k - p + 1); val prms = map (mk_ind_perm (n - i) k p (n - l) (("a", T) :: vs)) - (j - 1 downto 0) @ - map Bound (n - k downto n - k - p + 1) + (j - 1 downto 0) @ prms'; + val bs = rev (List.mapPartial + (fn ((_, T'), i) => if T = T' then SOME (Bound i) else NONE) + (List.take (vs, n - k - p - 1) ~~ (1 upto n - k - p - 1))); + val ts = map (fn i => + Const ("Nominal.supp", List.nth (Ts, n - i - 1) --> S) $ + foldr (mk_perm (T :: Ts)) (Bound (n - i)) prms') is in HOLogic.mk_Trueprop (Const ("Ex", (T --> HOLogic.boolT) --> HOLogic.boolT) $ Abs ("a", T, HOLogic.Not $ (Const ("op :", T --> S --> HOLogic.boolT) $ Bound 0 $ - (Const ("insert", T --> S --> S) $ - (foldr (mk_perm (T :: Ts)) (Bound (n - i - j)) prms) $ - (Const ("op Un", S --> S --> S) $ (f $ Bound (n - k - p)) $ - (Const ("Nominal.supp", U --> S) $ - foldr (mk_perm (T :: Ts)) (Bound (n - i')) prms)))))) + (foldr (fn (t, u) => Const ("insert", T --> S --> S) $ t $ u) + (foldl (fn (t, u) => Const ("op Un", S --> S --> S) $ u $ t) + (f $ Bound (n - k - p)) + (Const ("Nominal.supp", U --> S) $ + foldr (mk_perm (T :: Ts)) (Bound (n - i')) prms :: ts)) + (foldr (mk_perm (T :: Ts)) (Bound (n - i - j)) prms :: bs))))) end; fun mk_fresh_constr is p vs _ concl = @@ -1252,6 +1276,24 @@ val induct_aux_lemmas' = map (fn Type (s, _) => PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "2")) RS sym) dt_atomTs; + val fresh_aux = PureThy.get_thms thy9 (Name "fresh_aux"); + + (********************************************************************** + The subgoals occurring in the proof of induct_aux have the + following parameters: + + x_1 ... x_k p_1 ... p_m z b_1 ... b_n + + where + + x_i : constructor arguments (introduced by weak induction rule) + p_i : permutations (one for each atom type in the data type) + z : freshness context + b_i : newly introduced names for binders (sufficiently fresh) + ***********************************************************************) + + val _ = warning "proving strong induction theorem ..."; + val induct_aux = standard (Goal.prove thy9 [] ind_prems' ind_concl' (fn prems => EVERY ([mk_subgoal 1 (K (K (K aux_ind_concl))), @@ -1269,7 +1311,9 @@ in [mk_subgoal 1 (mk_fresh i (i + j) j' (length cargs) (length dt_atomTs) - (length cargs + length dt_atomTs + 1 + i - k)), + (length cargs + length dt_atomTs + 1 + i - k) + (List.mapPartial (fn (i', j) => + if i = i' then NONE else SOME (i' + j)) is)), rtac at_finite_select 1, rtac (PureThy.get_thm thy9 (Name ("at_" ^ atom ^ "_inst"))) 1, asm_full_simp_tac (simpset_of thy9 addsimps @@ -1286,14 +1330,19 @@ alpha @ abs_perm @ abs_fresh @ [abs_fun_finite_supp] @ induct_aux_lemmas)) 1, dtac sym 1, - asm_full_simp_tac (simpset_of thy9 - addsimps induct_aux_lemmas' - addsimprocs [perm_simproc]) 1, + asm_full_simp_tac (simpset_of thy9) 1, REPEAT (etac conjE 1)] else []) @ [(resolve_tac prems THEN_ALL_NEW - (atac ORELSE' ((REPEAT o etac allE) THEN' atac))) 1]) + (atac ORELSE' + SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of + _ $ (Const ("Nominal.fresh", _) $ _ $ _) => + asm_simp_tac (simpset_of thy9 addsimps fresh_aux) i + | _ => + asm_simp_tac (simpset_of thy9 + addsimps induct_aux_lemmas' + addsimprocs [perm_simproc]) i))) 1]) (constrs ~~ constrs'))) (descr'' ~~ ndescr)) @ [REPEAT (eresolve_tac [conjE, allE_Nil] 1), REPEAT (etac allE 1), @@ -1352,9 +1401,6 @@ (* introduction rules for graph of recursion function *) - fun partition_cargs idxs xs = map (fn (i, j) => - (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs; - fun mk_fresh_fun (a, t) = Const ("Nominal.fresh_fun", (fastype_of a --> fastype_of t) --> fastype_of t) $ lambda a t;