# HG changeset patch # User mueller # Date 873296686 -7200 # Node ID 0531f2c64c918efefc103b1ce5bc44087300c24c # Parent ebad042c0bba26dc120e98a8d993e9430b65616e new extended adm tactic introduced; diff -r ebad042c0bba -r 0531f2c64c91 src/HOLCF/Fix.ML --- a/src/HOLCF/Fix.ML Tue Sep 02 17:02:02 1997 +0200 +++ b/src/HOLCF/Fix.ML Wed Sep 03 16:24:46 1997 +0200 @@ -912,3 +912,8 @@ adm_iff]; Addsimps adm_lemmas; + +use"adm"; + +simpset := !simpset addSolver(fn thms => + (adm_tac (cut_facts_tac thms THEN' cont_tacRs))); diff -r ebad042c0bba -r 0531f2c64c91 src/HOLCF/Lift.ML --- a/src/HOLCF/Lift.ML Tue Sep 02 17:02:02 1997 +0200 +++ b/src/HOLCF/Lift.ML Wed Sep 03 16:24:46 1997 +0200 @@ -1,9 +1,16 @@ -open Lift; +(* Title: HOLCF/Lift.ML + ID: $Id$ + Author: Olaf Mueller + Copyright 1997 Technische Universitaet Muenchen + +Theorems for Lift.thy +*) + (* ---------------------------------------------------------- *) section"Continuity Proofs for flift1, flift2, if"; +(* ---------------------------------------------------------- *) (* need the instance into flat *) -(* ---------------------------------------------------------- *) (* flift1 is continuous in its argument itself*) diff -r ebad042c0bba -r 0531f2c64c91 src/HOLCF/adm.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/adm.ML Wed Sep 03 16:24:46 1997 +0200 @@ -0,0 +1,165 @@ +(******************* admissibility tactic *********************** + checks whether adm_subst theorem is applicable to the + current proof state. "t" is instantiated with a term of chain- + finite type, so that adm_chain_finite can be applied. + + example of usage: + + by (adm_tac cont_tacRs 1); + +*****************************************************************) + +local + +(*** find_subterms t 0 [] + returns lists of terms with the following properties: + 1. all terms in the list are disjoint subterms of t + 2. all terms contain the variable which is bound at level 0 + 3. all occurences of the variable which is bound at level 0 + are "covered" by a term in the list + a list of integers is associated with every term which describes + the "path" leading to the subterm (required for instantiation of + the adm_subst theorem (see functions mk_term, inst_adm_subst_thm)) +***) + +fun find_subterms (Bound i) lev path = + if i = lev then [[(Bound 0, path)]] + else [] + | find_subterms (t as (Abs (_, _, t2))) lev path = + if filter (fn x => x<=lev) + (add_loose_bnos (t, 0, [])) = [lev] then + [(incr_bv (~lev, 0, t), path)]:: + (find_subterms t2 (lev+1) (0::path)) + else find_subterms t2 (lev+1) (0::path) + | find_subterms (t as (t1 $ t2)) lev path = + let val ts1 = find_subterms t1 lev (0::path); + val ts2 = find_subterms t2 lev (1::path); + fun combine [] y = [] + | combine (x::xs) ys = + (map (fn z => x @ z) ys) @ (combine xs ys) + in + (if filter (fn x => x<=lev) + (add_loose_bnos (t, 0, [])) = [lev] then + [[(incr_bv (~lev, 0, t), path)]] + else []) @ + (if ts1 = [] then ts2 + else if ts2 = [] then ts1 + else combine ts1 ts2) + end + | find_subterms _ _ _ = []; + + +(*** make term for instantiation of predicate "P" in adm_subst theorem ***) + +fun make_term t path paths lev = + if path mem paths then Bound lev + else case t of + (Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1)) + | (t1 $ t2) => (make_term t1 (0::path) paths lev) $ + (make_term t2 (1::path) paths lev) + | t1 => t1; + + +(*** check whether all terms in list are equal ***) + +fun eq_terms (ts as ((t, _)::_)) = forall (fn (t2, _) => t2 aconv t) ts; + + +(*** NOTE: when the following two functions are called, all terms in the list + are equal (only their "paths" differ!) +***) + +(*** check whether type of terms in list is chain finite ***) + +fun is_chfin sign T params ((t, _)::_) = + let val {tsig, ...} = Sign.rep_sg sign; + val parTs = map snd (rev params) + in Type.of_sort tsig (fastype_of1 (T::parTs, t), ["chfin", "pcpo"]) end; + + +(*** try to prove that terms in list are continuous + if successful, add continuity theorem to list l ***) + +fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) = + (let val parTs = map snd (rev params); + val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT; + fun mk_all [] t = t + | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t)); + val t = HOLogic.mk_Trueprop ((Const ("cont", contT)) $ (Abs (s, T, t))); + val t' = mk_all params (Logic.list_implies (prems, t)); + val thm = prove_goalw_cterm [] (cterm_of sign t') + (fn ps => [cut_facts_tac ps 1, tac 1]) + in (ts, thm)::l end) handle _ => l; + + +(*** instantiation of adm_subst theorem (a bit tricky) + NOTE: maybe unnecessary (if "cont_thm RS adm_subst" works properly) ***) + +fun inst_adm_subst_thm state i params s T subt t paths = + let val {sign, maxidx, ...} = rep_thm state; + val j = maxidx+1; + val {tsig, ...} = Sign.rep_sg sign; + val parTs = map snd (rev params); + val rule = lift_rule (state, i) adm_subst; + val types = the o (fst (types_sorts rule)); + val tT = types ("t", j); + val PT = types ("P", j); + fun mk_abs [] t = t + | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t); + val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt); + val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))]) + (make_term t [] paths 0)); + val tye = Type.typ_match tsig ([], (tT, #T (rep_cterm tt))); + val tye' = Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt))); + val ctye = map (fn (x, y) => (x, ctyp_of sign y)) tye'; + val tv = cterm_of sign (Var (("t", j), typ_subst_TVars tye' tT)); + val Pv = cterm_of sign (Var (("P", j), typ_subst_TVars tye' PT)); + val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule + in rule' end; + + +(*** extract subgoal i from proof state ***) + +fun nth_subgoal i thm = nth_elem (i-1, prems_of thm); + + +in + +(*** the admissibility tactic + NOTE: + (compose_tac (false, rule, 2) i) THEN + (rtac cont_thm i) THEN ... + could probably be replaced by + (rtac (cont_thm RS adm_subst) 1) THEN ... +***) + +fun adm_tac tac i state = + state |> + let val goali = nth_subgoal i state + in + case Logic.strip_assums_concl goali of + ((Const _) $ ((Const ("adm", _)) $ (Abs (s, T, t)))) => + let val {sign, ...} = rep_thm state; + val prems = Logic.strip_assums_hyp goali; + val params = Logic.strip_params goali; + val ts = find_subterms t 0 []; + val ts' = filter eq_terms ts; + val ts'' = filter (is_chfin sign T params) ts'; + val thms = foldl (prove_cont tac sign s T prems params) ([], ts'') + in case thms of + ((ts as ((t', _)::_), cont_thm)::_) => + let val paths = map snd ts; + val rule = inst_adm_subst_thm state i params s T t' t paths; + in + (compose_tac (false, rule, 2) i) THEN + (rtac cont_thm i) THEN + (REPEAT (assume_tac i)) THEN + (rtac adm_chain_finite i) + end + | [] => no_tac + end + | _ => no_tac + end; + +end; +