1structure Witness :> Witness =
2struct
3
4open Abbrev;
5open NDDB
6
7val fun_all_rule = prove(``!P x.
8    fun_all P (\_. x) = P x
9``, bossLib.simp[fun_all_def]);
10
11(* GEN_TAC THEN GEN_TAC THEN DISCH_TAC THEN PURE_ONCE_REWRITE_TAC [fun_all_def] THEN GEN_TAC THEN BETA_TAC THEN (W (ACCEPT_TAC o mk_thm)));*)
12
13(************************* rules storage *************************)
14fun lookup tyvar (tyvar'::tyvars, h::dict) =
15    if tyvar = tyvar' then SOME h
16    else lookup tyvar (tyvars, dict)
17  | lookup _ _ = NONE;
18fun insert (tyvar, value) ([], []) = ([tyvar], [value])
19  | insert (tyvar, value) (tyvar'::tyvars, h::dict) =
20    if tyvar = tyvar' then (tyvar::tyvars, value::dict)
21    else let
22      val (x, y) = (insert (tyvar,value) (tyvars, dict))
23      in (tyvar'::x, h::y) end;
24val all_rules = ref (([]:string list),([]:Thm.thm list));
25
26val _ = (all_rules := insert ("sum_all", sum_all_def) (!all_rules);
27all_rules := insert ("list_all", list_all_def) (!all_rules);
28all_rules := insert ("prod_all", prod_all_def) (!all_rules);
29all_rules := insert ("option_all", option_all_def) (!all_rules);
30all_rules := insert ("fun_all", fun_all_rule) (!all_rules));
31
32(*load "finite_mapLib";
33all_rules := insert ("FEVERY", finite_mapTheory.FEVERY_DEF)
34                    (!all_rules);*)
35
36(*****************************************************************)
37
38fun variant thm = let
39  val vars = map type_of ((fst o strip_forall o concl) thm)
40  val vars' = map genvar vars
41  in SPECL vars' thm
42end;
43
44fun resolve q [] thm = []
45  | resolve q (rule::rules) thm = let
46        val (H, B) = dest_eq (concl rule)
47        val (H', H'') = dest_comb H
48        val (q', q'') = dest_comb q
49        val subst = match_term H' q'
50        val H'' = inst (#2 subst) H''
51        val d = INST_TY_TERM (match_term q'' H'') (DISCH q thm)
52        val rule' = INST_TY_TERM subst rule
53        val trans = IMP_TRANS (snd (EQ_IMP_RULE rule')) d
54        val hyps = (fst o dest_imp o concl) trans
55        val res = PROVE_HYP (ASSUME_CONJS hyps) (UNDISCH trans)
56      in res :: (resolve q rules thm)
57      end handle _ => resolve q rules thm;
58
59fun is_lit x = (is_const x) orelse (is_var x);
60fun dest_lit x = if is_const x then dest_const x else dest_var x;
61
62fun get_rules rules xrules tm =
63  if is_abs tm then let
64    val var = (genvar o fst o dom_rng o type_of) tm
65    in [BETA_CONV (mk_comb (tm, var))] end
66  else if is_const tm then
67    case lookup (#1 (dest_const tm)) rules of
68      NONE => raise ERR "" "unknown all fun"
69    | SOME thm => map variant (CONJUNCTS thm)
70  else if is_var tm then
71    case lookup (#1 (dest_var tm)) xrules of
72      NONE => raise ERR "" ""
73    | SOME thm => [thm]
74  else raise ERR "" "";
75
76fun REMOVE_EQ eq thm =
77     PROVE_HYP
78    (REFL (rhs eq))
79    (INST [(op|-> o dest_eq) eq] thm);
80
81fun leftmost alls xalls [     ] = raise ERR "Witness" "Empty type"
82  | leftmost alls xalls (t::ts) =
83      prove_all alls xalls t handle _ => leftmost alls xalls ts
84and prove_all alls xalls thm = let
85   val hs = hyp thm
86   val h1 = hd hs handle _ => T
87   in   if hs = []  then thm
88   else if h1 = T   then prove_all alls xalls (PROVE_HYP TRUTH thm)
89   else if is_eq h1 then prove_all alls xalls (REMOVE_EQ h1    thm)
90   else let val (ator, _) = strip_comb h1
91            val rules = get_rules alls xalls ator
92            val res = resolve h1 rules thm
93        in leftmost alls xalls res
94   end end;
95
96
97(*fun test q = let
98  val tm = Term q
99  val var = Term.variant (free_vars tm)
100            (mk_var ("x", (fst o dom_rng o type_of) tm))
101  val tm' = mk_comb(tm, var)
102  val res = prove_all (!all_rules) (ASSUME tm')
103  val wit = (snd o dest_comb o concl) res
104  val ex = mk_exists(var, tm')
105in EXISTS (ex, wit) res
106end;
107*)
108
109(*****************************************************************)
110(*
111prove_all (!all_rules) (ASSUME ``sum_all (\x.x=0) (prod_all (list_all P) (list_all Q)) x``)
112
113test`sum_all ($=0) (prod_all (list_all P) (list_all Q))`;
114test`option_all P`;
115test`sum_all (\_.F) (\_.F)`;
116test`fun_all (\_.T)`;
117
118val llrecycle = prove(``!x. ?ll. ll = x:::ll``,
119GEN_TAC THEN EXISTS_TAC
120
121Define`llx = 0:::llx`
122
123
124val all_llist_rule = prove(``P a ==> all_llist P (abs (\x. SOME a))``
125
126*)
127(*****************************************************************)
128
129
130local
131fun update_witnesses' [] [] _ _ = []
132  | update_witnesses' (NONE::wits) ((SOME t)::results) cs n =
133      (SOME (MATCH_MP (el n cs) t))
134      :: (update_witnesses' wits results cs (n+1))
135  | update_witnesses' (w::wits) (r::results) cs n =
136      w :: (update_witnesses' wits results cs (n+1))
137in fun update_witnesses cs w r = update_witnesses' w r cs 1
138end;
139
140fun foo (a,b) (c,d) = ((a@c), (b@d));
141
142fun update_wits_loop tms ws constrs = let
143    (* 1: extract known witnesses as rules  *)
144    val wrules = mapfilter (EQT_INTRO o valOf) ws
145    val ns = mapfilter(fst o dest_const o rator o concl o valOf)ws
146    (* 2: find new witnesses *)
147    val app = total (prove_all (foo (!all_rules) (ns, wrules)) ([],[]))
148    val ws' = map app tms
149    (* 3: update known witnesses *)
150    val func = fn (i, (wit, res)) => (
151        if (not (isSome wit)) andalso (isSome res) then
152           (SOME (MATCH_MP (el (i+1) constrs) (valOf res)))
153          else wit)
154    val ws'' = mapi (curry func) (zip ws ws')
155    (* 4: emptiness check *)
156    val _ = if map isSome ws = map isSome ws''
157            then raise ERR "gen_witness_repr" "Empty type"
158            else ()
159 in if   List.all isSome ws'
160    then ws''
161    else update_wits_loop tms ws'' constrs
162end;
163
164
165fun fix_ind_wits thm = let
166  val (a, b) = (dest_comb o concl) thm
167  val sub = map (fn x=> x|->((mk_arb o type_of)x)) (free_vars b)
168  val thm = INST sub thm
169  val (a, b) = (dest_comb o concl) thm
170  val var = Term.variant (free_vars a)
171            (mk_var ("x", type_of b))
172  val tm' = mk_comb(a, var)
173  val ex = mk_exists(var, tm')
174in EXISTS (ex, b) thm
175end;
176
177fun find_inductive_witnesses a b c = let
178    val res = update_wits_loop a b c
179  in map (fix_ind_wits o valOf) res
180end;
181
182(*
183fun test2 thm = let
184  val res = prove_all (!all_rules) thm
185  val wit = (snd o dest_comb o concl) res
186  val sub = map (fn x=> x|->((mk_arb o type_of)x)) (free_vars wit)
187in INST sub res
188end;
189
190
191val Hyps = [``(list_all P x):bool``, ``(sum_all (XX:'a list->bool) YY x):bool``];
192
193
194val ws = [NONE, NONE];
195val constrs = [mk_thm([], ``!P x. (list_all P x) ==> (XX x)``),
196mk_thm([], ``!XX YY x. (sum_all (XX:'a list->bool) YY x) ==> ZZ x``)]
197val Hyps = map(fst o dest_imp o snd o strip_forall o concl) constrs
198val tms = (map ASSUME Hyps)
199update_wits_loop tms ws constrs
200
201prove_all alls xalls thm
202
203
204val ax = mk_thm([], ``!P x. (list_all P x) ==> (XX x)``);
205UNDISCH (SPEC_ALL ax);
206
207*)
208
209
210end;
211