# HG changeset patch # User wenzelm # Date 978899734 -3600 # Node ID 8b2eafed618352bc0314ef8b71fc0eecd139a40a # Parent dd5fb02ff87208cc1b3ccd893a1102ebe64a9ae2 added is_norm_hhf; diff -r dd5fb02ff872 -r 8b2eafed6183 src/Pure/logic.ML --- a/src/Pure/logic.ML Sun Jan 07 21:35:11 2001 +0100 +++ b/src/Pure/logic.ML Sun Jan 07 21:35:34 2001 +0100 @@ -45,6 +45,7 @@ val strip_assums_hyp : term -> term list val strip_assums_concl: term -> term val strip_params : term -> (string * typ) list + val is_norm_hhf : term -> bool val has_meta_prems : term -> int -> bool val flatten_params : int -> term -> term val auto_rename : bool ref @@ -252,6 +253,12 @@ | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t | strip_params B = []; +(*test for HHF normal form*) +fun is_norm_hhf (Const ("==>", _) $ _ $ (Const ("all", _) $ _)) = false + | is_norm_hhf (t $ u) = is_norm_hhf t andalso is_norm_hhf u + | is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t + | is_norm_hhf _ = true; + (*test for meta connectives in prems of a 'subgoal'*) fun has_meta_prems prop i = let @@ -320,8 +327,8 @@ We need nparams_i only when the parameters aren't flattened; then we must call incr_boundvars to make up the difference. See assum_pairs. Without this refinement we can get the wrong answer, e.g. by - Goal "!!f. EX B. Q(f,B) ==> (!!y. P(f,y))"; - by (etac exE 1); + Goal "!!f. EX B. Q(f,B) ==> (!!y. P(f,y))"; + by (etac exE 1); *) fun strip_assums_aux (HPs, params, Const("==>", _) $ H $ B) = strip_assums_aux ((H,length params)::HPs, params, B) @@ -339,12 +346,12 @@ let val (HPs, params, B) = strip_assums A val nparams = length params val D = Unify.rlist_abs(params, B) - fun incr_hyp(H,np) = - Unify.rlist_abs(params, incr_boundvars (nparams-np) H) + fun incr_hyp(H,np) = + Unify.rlist_abs(params, incr_boundvars (nparams-np) H) fun pairrev ([],pairs) = pairs | pairrev ((H,np)::HPs, pairs) = pairrev(HPs, (incr_hyp(H,np),D) :: pairs) - in pairrev (HPs,[]) + in pairrev (HPs,[]) end; (*Converts Frees to Vars and TFrees to TVars so that axioms can be written