1structure Rules :> Rules =
2struct
3
4open HolKernel boolLib pairLib wfrecUtils;
5
6
7val ERR = mk_HOL_ERR "Rules";
8
9fun sthat P x = P x handle Interrupt => raise Interrupt
10                         |     _     => false;
11
12fun simpl_conv thl =
13  let open RW
14      val RWC = Rewrite Fully
15                   (Simpls(std_simpls,thl),
16                    Context([],DONT_ADD),
17                    Congs[boolTheory.IMP_CONG],
18                    Solver always_fails)
19      fun simpl tm =
20       let val th = Conv.THENC(RWC,Conv.DEPTH_CONV GEN_BETA_CONV) tm
21           val (lhs,rhs) = dest_eq(concl th)
22       in if aconv lhs rhs then th else TRANS th (simpl rhs)
23       end
24  in simpl
25  end;
26
27fun is_triv_rw tm = uncurry aconv (dest_eq tm) handle HOL_ERR _ => false;
28
29fun non_triv thl = filter (not o is_triv_rw o concl) thl
30
31(*---------------------------------------------------------------------------*)
32(* PURE_REWRITE_RULE plus generalized beta conversion.                       *)
33(*---------------------------------------------------------------------------*)
34
35fun simplify thl =
36 let val rewrite = PURE_REWRITE_RULE (non_triv thl) (* PURE_ONCE_REWRITE_RULE *)
37     fun simpl th =
38      let val th' = GEN_BETA_RULE (rewrite th)
39          val (_,c1) = dest_thm th
40          val (_,c2) = dest_thm th'
41      in if aconv c1 c2 then th else simpl th'
42      end
43 in simpl
44 end;
45
46val RIGHT_ASSOC = PURE_REWRITE_RULE [GSYM boolTheory.DISJ_ASSOC];
47
48fun FILTER_DISCH_ALL P th = itlist DISCH (filter (sthat P) (Thm.hyp th)) th;
49
50(*----------------------------------------------------------------------------
51 *
52 *         A |- M
53 *   -------------------   [v_1,...,v_n]
54 *    A |- ?v1...v_n. M
55 *
56 *---------------------------------------------------------------------------*)
57
58fun EXISTL vlist thm =
59   itlist (fn v => fn thm => EXISTS(mk_exists(v,concl thm),v) thm)
60          vlist thm;
61
62(*----------------------------------------------------------------------------
63 *
64 *       A |- M[x_1,...,x_n]
65 *   ----------------------------   [(x |-> y)_1,...,(x |-> y)_n]
66 *       A |- ?y_1...y_n. M
67 *
68 *---------------------------------------------------------------------------*)
69
70fun IT_EXISTS theta thm =
71 itlist (fn (b as {redex,residue}) => fn thm =>
72           EXISTS(mk_exists(residue, subst [b] (concl thm)), redex) thm)
73        theta thm;
74
75(*----------------------------------------------------------------------------
76 *
77 *                   A1 |- M1, ..., An |- Mn
78 *     ---------------------------------------------------
79 *     [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
80 *
81 *---------------------------------------------------------------------------*)
82
83fun EVEN_ORS thms =
84  let fun blue ldisjs [] _ = []
85        | blue ldisjs (th::rst) rdisjs =
86            let val rdisj_tl = list_mk_disj(Lib.trye tl rdisjs)
87            in itlist DISJ2 ldisjs (DISJ1 th rdisj_tl)
88               :: blue (ldisjs@[concl th]) rst (Lib.trye tl rdisjs)
89            end
90            handle HOL_ERR _ => [itlist DISJ2 ldisjs th]
91   in
92   blue [] thms (map concl thms)
93   end;
94
95(*---------------------------------------------------------------------------*)
96(*                                                                           *)
97(*         v = pat[v1,...,vn]  |- M[x]                                       *)
98(*    ------------------------------------------                             *)
99(*      ?v1 ... vn. v = pat[v1,...,vn] |- M[x]                               *)
100(*                                                                           *)
101(*---------------------------------------------------------------------------*)
102
103fun CHOOSER v (tm,thm) =
104 let val ex_tm = mk_exists(v,tm)
105 in (ex_tm, CHOOSE(v, ASSUME ex_tm) thm)
106 end;
107
108fun LEFT_ABS_VSTRUCT thm =
109 let open boolSyntax
110     val veq = Lib.trye hd (filter (can dest_eq) (Thm.hyp thm))
111     val pat = rhs veq
112 in snd(itlist CHOOSER (free_vars_lr pat) (veq,thm))
113 end;
114
115(*---------------------------------------------------------------------------*)
116(*                                                                           *)
117(*      Gamma, (x = pat[v1,...,vn]) /\ constraints |- M[x]                   *)
118(*    ------------------------------------------------------------------     *)
119(*      Gamma, ?v1 ... vn. (x = pat[v1,...,vn]) /\ constraints |- M[x]       *)
120(*                                                                           *)
121(*---------------------------------------------------------------------------*)
122
123fun LEFT_EXISTS thm =
124 case filter (can (dest_eq o hd o strip_conj)) (Thm.hyp thm)
125  of [] => raise ERR "LEFT_EXISTS" "expected an eqn in hyps"
126   | veq_conj :: _ =>
127     let val (_,pat) = dest_eq (hd (strip_conj veq_conj))
128     in snd (itlist CHOOSER (free_vars_lr pat) (veq_conj,thm))
129     end;
130
131end (* Rules *)
132