36 (***********************************************************************************) |
36 (***********************************************************************************) |
37 |
37 |
38 val anyt = Free ("t", TFree ("'t", [])); |
38 val anyt = Free ("t", TFree ("'t", [])); |
39 |
39 |
40 fun strong_ind_simproc tab = |
40 fun strong_ind_simproc tab = |
41 Simplifier.simproc_global_i @{theory HOL} "strong_ind" [anyt] (fn ctxt => fn t => |
41 Simplifier.make_simproc @{context} "strong_ind" |
42 let |
42 {lhss = [@{term "x::'a::{}"}], |
43 fun close p t f = |
43 proc = fn _ => fn ctxt => fn ct => |
44 let val vs = Term.add_vars t [] |
44 let |
45 in Thm.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs)) |
45 fun close p t f = |
46 (p (fold (Logic.all o Var) vs t) f) |
46 let val vs = Term.add_vars t [] |
47 end; |
47 in Thm.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs)) |
48 fun mkop @{const_name HOL.conj} T x = |
48 (p (fold (Logic.all o Var) vs t) f) |
49 SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x) |
49 end; |
50 | mkop @{const_name HOL.disj} T x = |
50 fun mkop @{const_name HOL.conj} T x = |
51 SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x) |
51 SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x) |
52 | mkop _ _ _ = NONE; |
52 | mkop @{const_name HOL.disj} T x = |
53 fun mk_collect p T t = |
53 SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x) |
54 let val U = HOLogic.dest_setT T |
54 | mkop _ _ _ = NONE; |
55 in HOLogic.Collect_const U $ |
55 fun mk_collect p T t = |
56 HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t |
56 let val U = HOLogic.dest_setT T |
57 end; |
57 in HOLogic.Collect_const U $ |
58 fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member}, |
58 HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t |
59 Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) = |
59 end; |
60 mkop s T (m, p, S, mk_collect p T (head_of u)) |
60 fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member}, |
61 | decomp (Const (s, _) $ u $ ((m as Const (@{const_name Set.member}, |
61 Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) = |
62 Type (_, [_, Type (_, [T, _])]))) $ p $ S)) = |
62 mkop s T (m, p, S, mk_collect p T (head_of u)) |
63 mkop s T (m, p, mk_collect p T (head_of u), S) |
63 | decomp (Const (s, _) $ u $ ((m as Const (@{const_name Set.member}, |
64 | decomp _ = NONE; |
64 Type (_, [_, Type (_, [T, _])]))) $ p $ S)) = |
65 val simp = |
65 mkop s T (m, p, mk_collect p T (head_of u), S) |
66 full_simp_tac |
66 | decomp _ = NONE; |
67 (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]) 1; |
67 val simp = |
68 fun mk_rew t = (case strip_abs_vars t of |
68 full_simp_tac |
69 [] => NONE |
69 (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]) 1; |
70 | xs => (case decomp (strip_abs_body t) of |
70 fun mk_rew t = (case strip_abs_vars t of |
71 NONE => NONE |
71 [] => NONE |
72 | SOME (bop, (m, p, S, S')) => |
72 | xs => (case decomp (strip_abs_body t) of |
73 SOME (close (Goal.prove ctxt [] []) |
73 NONE => NONE |
74 (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S')))) |
74 | SOME (bop, (m, p, S, S')) => |
75 (K (EVERY |
75 SOME (close (Goal.prove ctxt [] []) |
76 [resolve_tac ctxt [eq_reflection] 1, |
76 (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S')))) |
77 REPEAT (resolve_tac ctxt @{thms ext} 1), |
77 (K (EVERY |
78 resolve_tac ctxt [iffI] 1, |
78 [resolve_tac ctxt [eq_reflection] 1, |
79 EVERY [eresolve_tac ctxt [conjE] 1, resolve_tac ctxt [IntI] 1, simp, simp, |
79 REPEAT (resolve_tac ctxt @{thms ext} 1), |
80 eresolve_tac ctxt [IntE] 1, resolve_tac ctxt [conjI] 1, simp, simp] ORELSE |
80 resolve_tac ctxt [iffI] 1, |
81 EVERY [eresolve_tac ctxt [disjE] 1, resolve_tac ctxt [UnI1] 1, simp, |
81 EVERY [eresolve_tac ctxt [conjE] 1, resolve_tac ctxt [IntI] 1, simp, simp, |
82 resolve_tac ctxt [UnI2] 1, simp, |
82 eresolve_tac ctxt [IntE] 1, resolve_tac ctxt [conjI] 1, simp, simp] ORELSE |
83 eresolve_tac ctxt [UnE] 1, resolve_tac ctxt [disjI1] 1, simp, |
83 EVERY [eresolve_tac ctxt [disjE] 1, resolve_tac ctxt [UnI1] 1, simp, |
84 resolve_tac ctxt [disjI2] 1, simp]]))) |
84 resolve_tac ctxt [UnI2] 1, simp, |
85 handle ERROR _ => NONE)) |
85 eresolve_tac ctxt [UnE] 1, resolve_tac ctxt [disjI1] 1, simp, |
86 in |
86 resolve_tac ctxt [disjI2] 1, simp]]))) |
87 case strip_comb t of |
87 handle ERROR _ => NONE)) |
88 (h as Const (name, _), ts) => (case Symtab.lookup tab name of |
88 in |
89 SOME _ => |
89 (case strip_comb (Thm.term_of ct) of |
90 let val rews = map mk_rew ts |
90 (h as Const (name, _), ts) => |
91 in |
91 if Symtab.defined tab name then |
92 if forall is_none rews then NONE |
92 let val rews = map mk_rew ts |
93 else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1) |
93 in |
94 (map2 (fn SOME r => K r | NONE => Thm.reflexive o Thm.cterm_of ctxt) |
94 if forall is_none rews then NONE |
95 rews ts) (Thm.reflexive (Thm.cterm_of ctxt h))) |
95 else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1) |
96 end |
96 (map2 (fn SOME r => K r | NONE => Thm.reflexive o Thm.cterm_of ctxt) |
97 | NONE => NONE) |
97 rews ts) (Thm.reflexive (Thm.cterm_of ctxt h))) |
98 | _ => NONE |
98 end |
99 end); |
99 else NONE |
|
100 | _ => NONE) |
|
101 end, |
|
102 identifier = []}; |
100 |
103 |
101 (* only eta contract terms occurring as arguments of functions satisfying p *) |
104 (* only eta contract terms occurring as arguments of functions satisfying p *) |
102 fun eta_contract p = |
105 fun eta_contract p = |
103 let |
106 let |
104 fun eta b (Abs (a, T, body)) = |
107 fun eta b (Abs (a, T, body)) = |