1structure Opening :>  Opening =
2struct
3
4open HolKernel boolLib liteLib Trace;
5
6
7fun samerel t1 t2 = can (match_term t1) t2
8
9type congproc  = {relation:term,
10                  solver : term -> thm,
11                  freevars: term list,
12                  depther : thm list * term -> conv} -> conv
13
14
15fun WRAP_ERR x = STRUCT_WRAP "Opening" x;
16fun ERR x = STRUCT_ERR "Opening" x;
17
18(* ---------------------------------------------------------------------
19 * is_congruence
20 *    Test if a term is a valid conclusion of a congruence rule,
21 *
22 * EXAMPLES
23 *   is_congruence (--`(A ==> B) = (A' ==> B')`--);
24 *   is_congruence (--`(A ==> B) ==> (A' ==> B')`--);
25 *   is_congruence (--`(A ==> B) <== (A' ==> B')`--);
26 *   is_congruence (--`(!x:'a. P x) <== (!x:'a. P' x)`--);
27 *   is_congruence (--`(A <== A') ==> (A ==> B) ==> (A' ==> B')`--); (*false*)
28 *
29 * rel_of_congruence
30 *   Discover the relation a congruence is expressed over.
31 *
32 * EXAMPLES
33 *   rel_of_congrule imp_imp_rule;
34 *   rel_of_congrule imp_pmi_rule;
35 *   rel_of_congrule pmi_imp_rule;
36 *   rel_of_congrule pmi_neg_rule;
37 *   rel_of_congrule imp_forall_rule;
38 *
39 * nconds_of_congrule
40 *   Discover how many side conditions a congruence rule has.  Nb. Can't
41 * just call strip_imp as the congruence may be expressed over (--`$==>`--)
42 *
43 *   nconds_of_congrule imp_imp_rule;  (* 2 *)
44 *   nconds_of_congrule imp_pmi_rule;  (* 2 *)
45 *   nconds_of_congrule pmi_imp_rule;  (* 2 *)
46 *   nconds_of_congrule pmi_neg_rule;  (* 1 *)
47 *   nconds_of_congrule pmi_forall_rule;  (* 1 *)
48 *   nconds_of_congrule imp_forall_rule;  (* 1 *)
49 * ---------------------------------------------------------------------*)
50
51fun dest_binop t = let
52  val (fx,y) = dest_comb t
53  val (f,x) = dest_comb fx
54in
55  (f,x,y)
56end
57
58fun is_congruence tm =
59    is_eq tm orelse let
60      val (rel,left,right) = dest_binop tm
61    in
62      (can (ho_match_term [] empty_tmset left) right) andalso
63      (can (ho_match_term [] empty_tmset right) left)
64    end
65   handle HOL_ERR _ => false
66
67fun rel_of_congrule thm = let
68  fun aux tm = if is_congruence tm then #1 (dest_binop tm)
69               else aux (snd (dest_imp tm))
70in
71  aux (snd(strip_forall (concl thm)))
72end handle e => WRAP_ERR("rel_of_congrule",e)
73
74fun nconds_of_congrule thm = let
75  fun aux tm = if is_congruence tm then 0 else aux (snd(dest_imp tm)) + 1
76in
77  aux (snd(strip_forall(concl thm)))
78end handle e => WRAP_ERR("nconds_of_congrule",e)
79
80(* ---------------------------------------------------------------------
81 * CONGPROC : REFL -> congrule -> congproc
82 *
83 * ---------------------------------------------------------------------*)
84
85fun strip_n_imp 0 tm = ([],tm)
86  | strip_n_imp n tm =
87      let val (x,y) = dest_imp tm
88          val (z,w) = strip_n_imp (n-1) y
89      in (x::z,w)
90      end;
91
92(* ---------------------------------------------------------------------
93 * strip_imp_until_rel
94 *
95 * this function strips implications off a sub-congruence until
96 * it is a relation (i.e. the rhs is one of the genvars we have chosen)
97 * or it is no longer an implication (in which case the sub-congruence
98 * is really a side condition.
99 *
100 * ---------------------------------------------------------------------*)
101
102
103fun strip_imp_until_rel genvars tm =
104     (if (is_var (rand tm) andalso mem (rand tm) genvars)
105     then ([],tm)
106     else let val (x,y) = dest_imp tm
107              val (z,w) = strip_imp_until_rel genvars y
108          in (x::z,w)
109          end)
110     handle HOL_ERR _ => ([],tm);
111
112(* ---------------------------------------------------------------------
113 * CONGPROC : REFL -> congrule -> congproc
114 *
115 * ---------------------------------------------------------------------*)
116
117val equality = boolSyntax.equality
118
119fun CONGPROC refl congrule =
120let
121
122   (* this discharges each antecedent of the congruence rule.  Each
123      antecedent is either a side condition or a sub-congruence.
124      Side conditions must be passed to the solver, sub-congruences
125      must be passed to the depther. *)
126
127   val congrule' = GSPEC (GEN_ALL congrule)
128   val nconds = nconds_of_congrule congrule'
129   val rel = rel_of_congrule congrule'
130
131   val (conditions,conc) = strip_n_imp nconds (concl congrule')
132   val matcher =
133      HO_PART_MATCH (rator o snd o strip_n_imp nconds) congrule'
134
135 (* work out whether context assumptions need to be reprocessed *)
136 (* e.g "~g" in the "else" branch of COND_CONG needs to be.     *)
137
138   val vars = free_vars (concl congrule')
139   fun reprocess_flag assum = if is_var assum then false else true;
140   val reprocess_flags =
141       map (map reprocess_flag o fst o strip_imp_until_rel vars o
142            #2 o strip_forall)
143           conditions
144
145in fn {relation,solver,depther,freevars} =>
146  if not (samerel rel relation) andalso not (same_const rel relation) then
147    failwith "not applicable"
148  else fn tm =>
149  let
150    val theta = match_type (#1 (dom_rng (type_of relation))) (type_of tm)
151    val relation' = Term.inst theta relation
152    val match_thm = matcher (mk_comb(relation',tm))
153    val _ = trace(3,OPENING(tm,match_thm))
154    val (_,conc) = strip_n_imp nconds (concl match_thm)
155    val genvars = filter is_genvar (free_vars (rand conc))
156
157    (* this function does all the work of solving the side conditions
158       one by one.  The integer is the number of side conditions
159       remaining to be discharged.  Most of the side conditions
160       will be sub-congruences of the form (--`A = ?A`--)  *)
161
162    fun process_subgoals (0,match_thm,_) = match_thm
163      | process_subgoals (_,_,[]) = raise Fail "process_subgoals BIND"
164      | process_subgoals (n,match_thm,flags::more_flags) =
165        let val condition = #1 (dest_imp (concl match_thm))
166
167           (* work out whether the condition is a congruence condition
168              or a side condition.  If it is two place and the
169              head combinator of the rhs is one of the subterms
170              in the congruence (see subterms above) then it
171              is a congruence condition *)
172            val (ho_vars,bdy1) = strip_forall condition
173            val (assums,bdy2) = strip_imp_until_rel genvars bdy1
174            val (oper,args) = let
175              val (f,x,y) = dest_binop bdy2
176            in
177              (f,[x,y])
178            end handle HOL_ERR _ => strip_comb bdy2
179        in
180          if length args = 2 andalso mem (#1 (strip_comb (el 2 args))) genvars
181          then let
182                val (orig,res) = case args of [x,y] => (x,y) | _ => raise Bind
183                val genv = #1 (strip_comb res)
184                val assum_thms = map ASSUME assums
185                fun reprocess thm flag =
186                  if flag then CONV_RULE (depther ([],equality)) thm
187                    handle HOL_ERR _ =>
188                    (trace(5,PRODUCE(concl thm,"UNCHANGED",thm));thm)
189                  else thm
190                val reprocessed_assum_thms = map2 reprocess assum_thms flags
191                val rewr_thm =
192                  (depther (reprocessed_assum_thms,oper) orig)
193                  handle HOL_ERR _ =>
194                  let val thm = refl {Rinst = oper, arg = orig}
195                  in (trace(5,PRODUCE(orig,"UNCHANGED",thm));thm)
196                  end
197                val abs_rewr_thm =
198                    CONV_RULE (RAND_CONV (MK_ABSL_CONV ho_vars)) rewr_thm
199                val disch_abs_rewr_thm = itlist DISCH assums abs_rewr_thm
200                val gen_abs_rewr_thm = GENL ho_vars disch_abs_rewr_thm
201                val gen_abs_res =
202                    funpow (length ho_vars) rator (rand (concl abs_rewr_thm))
203                val spec_match_thm = SPEC gen_abs_res (GEN genv match_thm)
204                val new_match_thm = MP spec_match_thm gen_abs_rewr_thm
205            in process_subgoals (n-1,new_match_thm,more_flags)
206            end
207          else let
208              fun output() =
209                  "Instantiated congruence condition is a side condition: "^
210                  term_to_string condition
211              val _ = trace (6, LZ_TEXT output)
212              val side_condition_thm = solver condition
213              val new_match_thm = MP match_thm side_condition_thm
214            in process_subgoals (n-1,new_match_thm,more_flags)
215            end
216        end
217
218    val final_thm = process_subgoals (nconds,match_thm,reprocess_flags)
219
220  in
221    if (rand (rator (concl final_thm)) = rand (concl final_thm))
222      then raise HOL_ERR { origin_structure = "Opening",
223                           origin_function = "CONGPROC",
224                           message = "Congruence gives no change" }
225    else (trace(3,PRODUCE(tm,"congruence rule",final_thm)); final_thm)
226  end
227end;
228
229
230(* ---------------------------------------------------------------------
231 * EQ_CONGPROC
232 *
233 *  Opening through HOL terms under HOL equality.
234 * ---------------------------------------------------------------------*)
235
236fun EQ_CONGPROC {relation,depther,solver,freevars} tm =
237 if not (same_const relation boolSyntax.equality) then failwith "not applicable"
238 else
239 case dest_term tm
240  of COMB(Rator,Rand) =>
241      (let val th = depther ([],equality) Rator
242      in  MK_COMB (th, depther ([],equality)  Rand)
243        handle HOL_ERR _ => AP_THM th Rand
244      end
245       handle HOL_ERR _ => AP_TERM Rator (depther ([],equality)  Rand))
246   | LAMB(Bvar,Body) =>
247     if mem Bvar freevars then
248     let val v = variant (freevars@free_vars Body) Bvar
249         val th1 = ALPHA_CONV v tm handle e as HOL_ERR _
250         => (trace(0,REDUCE("SIMPLIFIER ERROR: bug when alpha converting",tm));
251             trace(0,REDUCE("trying to alpha convert to",v));
252             Raise e)
253         val rhs' = rhs(concl th1)
254         val Body' = body rhs' (* v = Bvar *)
255         val body_thm = depther ([],equality) Body'
256         val eq_thm' = ABS v body_thm
257     in
258        TRANS th1 eq_thm'
259     end
260     else let val _ = trace(4,TEXT "no alpha conversion")
261              val Bth = depther ([],equality) Body
262          in ABS Bvar Bth
263          end
264   | _ => failwith "unchanged";
265
266
267end (* struct *)
268