# HG changeset patch # User berghofe # Date 1035212847 -7200 # Node ID 3cf622f6b0b2cc08608476fb31bb2b0c21593575 # Parent c9ad3e64ddcfa59405f204b1f3c4d86c6b305457 Removed obsolete functions dealing with flex-flex constraints. diff -r c9ad3e64ddcf -r 3cf622f6b0b2 src/Pure/drule.ML --- a/src/Pure/drule.ML Mon Oct 21 17:04:47 2002 +0200 +++ b/src/Pure/drule.ML Mon Oct 21 17:07:27 2002 +0200 @@ -14,7 +14,6 @@ val list_implies : cterm list * cterm -> cterm val dest_implies : cterm -> cterm * cterm val dest_equals : cterm -> cterm * cterm - val skip_flexpairs : cterm -> cterm val strip_imp_prems : cterm -> cterm list val strip_imp_concl : cterm -> cterm val cprems_of : thm -> cterm list @@ -69,7 +68,6 @@ val swap_prems_eq : thm val equal_abs_elim : cterm -> thm -> thm val equal_abs_elim_list: cterm list -> thm -> thm - val flexpair_abs_elim_list: cterm list -> thm -> thm val asm_rl : thm val cut_rl : thm val revcut_rl : thm @@ -159,13 +157,6 @@ | _ => raise TERM ("dest_equals", [term_of ct]) ; -(*Discard flexflex pairs; return a cterm*) -fun skip_flexpairs ct = - case term_of ct of - (Const("==>", _) $ (Const("=?=",_)$_$_) $ _) => - skip_flexpairs (#2 (dest_implies ct)) - | _ => ct; - (* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) fun strip_imp_prems ct = let val (cA,cB) = dest_implies ct @@ -179,7 +170,7 @@ | _ => ct; (*The premises of a theorem, as a cterm list*) -val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of; +val cprems_of = strip_imp_prems o cprop_of; val proto_sign = Theory.sign_of ProtoPure.thy; @@ -403,16 +394,16 @@ Similar code in type/freeze_thaw*) fun freeze_thaw th = let val fth = freezeT th - val {prop,sign,...} = rep_thm fth + val {prop, tpairs, sign, ...} = rep_thm fth in - case term_vars prop of + case foldr add_term_vars (prop :: Thm.terms_of_tpairs tpairs, []) of [] => (fth, fn x => x) | vars => let fun newName (Var(ix,_), (pairs,used)) = let val v = variant used (string_of_indexname ix) in ((ix,v)::pairs, v::used) end; - val (alist, _) = foldr newName - (vars, ([], add_term_names (prop, []))) + val (alist, _) = foldr newName (vars, ([], foldr add_term_names + (prop :: Thm.terms_of_tpairs tpairs, []))) fun mk_inst (Var(v,T)) = (cterm_of sign (Var(v,T)), cterm_of sign (Free(the (assoc(alist,v)), T))) @@ -791,27 +782,6 @@ (*Calling equal_abs_elim with multiple terms*) fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th); -local - val alpha = TVar(("'a",0), []) (* type ?'a::{} *) - fun err th = raise THM("flexpair_inst: ", 0, [th]) - fun flexpair_inst def th = - let val {prop = Const _ $ t $ u, sign,...} = rep_thm th - val cterm = cterm_of sign - fun cvar a = cterm(Var((a,0),alpha)) - val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)] - def - in equal_elim def' th - end - handle THM _ => err th | Bind => err th -in -val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def) -and flexpair_elim = flexpair_inst ProtoPure.flexpair_def -end; - -(*Version for flexflex pairs -- this supports lifting.*) -fun flexpair_abs_elim_list cts = - flexpair_intr o equal_abs_elim_list cts o flexpair_elim; - (*** Goal (PROP A) <==> PROP A ***) diff -r c9ad3e64ddcf -r 3cf622f6b0b2 src/Pure/logic.ML --- a/src/Pure/logic.ML Mon Oct 21 17:04:47 2002 +0200 +++ b/src/Pure/logic.ML Mon Oct 21 17:07:27 2002 +0200 @@ -24,13 +24,7 @@ val count_prems : term * int -> int val mk_conjunction : term * term -> term val mk_conjunction_list: term list -> term - val mk_flexpair : term * term -> term - val dest_flexpair : term -> term * term - val list_flexpairs : (term*term)list * term -> term - val rule_of : (term*term)list * term list * term -> term - val strip_flexpairs : term -> (term*term)list * term - val skip_flexpairs : term -> term - val strip_horn : term -> (term*term)list * term list * term + val strip_horn : term -> term list * term val mk_cond_defpair : term list -> term * term -> string * term val mk_defpair : term * term -> string * term val mk_type : typ -> term @@ -118,6 +112,10 @@ fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1) | count_prems (_,n) = n; +(*strip a proof state (Horn clause): + B1 ==> ... Bn ==> C goes to ([B1, ..., Bn], C) *) +fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); + (** conjunction **) @@ -128,45 +126,6 @@ | mk_conjunction_list ts = foldr1 mk_conjunction ts; -(** flex-flex constraints **) - -(*Make a constraint.*) -fun mk_flexpair(t,u) = flexpair(fastype_of t) $ t $ u; - -fun dest_flexpair (Const("=?=",_) $ t $ u) = (t,u) - | dest_flexpair t = raise TERM("dest_flexpair", [t]); - -(*make flexflex antecedents: ( [(a1,b1),...,(an,bn)] , C ) - goes to (a1=?=b1) ==>...(an=?=bn)==>C *) -fun list_flexpairs ([], A) = A - | list_flexpairs ((t,u)::pairs, A) = - implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A); - -(*Make the object-rule tpairs==>As==>B *) -fun rule_of (tpairs, As, B) = list_flexpairs(tpairs, list_implies(As, B)); - -(*Remove and return flexflex pairs: - (a1=?=b1)==>...(an=?=bn)==>C to ( [(a1,b1),...,(an,bn)] , C ) - [Tail recursive in order to return a pair of results] *) -fun strip_flex_aux (pairs, Const("==>", _) $ (Const("=?=",_)$t$u) $ C) = - strip_flex_aux ((t,u)::pairs, C) - | strip_flex_aux (pairs,C) = (rev pairs, C); - -fun strip_flexpairs A = strip_flex_aux([], A); - -(*Discard flexflex pairs*) -fun skip_flexpairs (Const("==>", _) $ (Const("=?=",_)$_$_) $ C) = - skip_flexpairs C - | skip_flexpairs C = C; - -(*strip a proof state (Horn clause): - (a1==b1)==>...(am==bm)==>B1==>...Bn==>C - goes to ( [(a1,b1),...,(am,bm)] , [B1,...,Bn] , C) *) -fun strip_horn A = - let val (tpairs,horn) = strip_flexpairs A - in (tpairs, strip_imp_prems horn, strip_imp_concl horn) end; - - (** definitions **) fun mk_cond_defpair As (lhs, rhs) = @@ -270,9 +229,8 @@ | is_meta (Const ("==", _) $ _ $ _) = true | is_meta (Const ("all", _) $ _) = true | is_meta _ = false; - val horn = skip_flexpairs prop; in - (case strip_prems (i, [], horn) of + (case strip_prems (i, [], prop) of (B :: _, _) => exists is_meta (strip_assums_hyp B) | _ => false) handle TERM _ => false end;