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