Removed obsolete functions dealing with flex-flex constraints.
--- 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 ***)
--- 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;