ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
authorlcp
Thu Aug 18 17:41:40 1994 +0200 (1994-08-18 ago)
changeset 543e961b2092869
parent 542 164be35c8a16
child 544 c53386a5bcf1
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
ZF/ind_syntax/prove_term: deleted

ZF/constructor, indrule, intr_elim: now call prove_goalw_cterm and
Logic.unvarify
src/ZF/constructor.ML
src/ZF/ind_syntax.ML
src/ZF/indrule.ML
src/ZF/intr_elim.ML
     1.1 --- a/src/ZF/constructor.ML	Thu Aug 18 12:56:57 1994 +0200
     1.2 +++ b/src/ZF/constructor.ML	Thu Aug 18 17:41:40 1994 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5  (*Get the case term from its definition*)
     1.6  val Const("==",_) $ big_case_tm $ _ =
     1.7 -    hd con_defs |> rep_thm |> #prop |> unvarify;
     1.8 +    hd con_defs |> rep_thm |> #prop |> Logic.unvarify;
     1.9  
    1.10  val (_, big_case_args) = strip_comb big_case_tm;
    1.11  
    1.12 @@ -62,8 +62,9 @@
    1.13  			Su.case_inr RS trans] 1)];
    1.14  
    1.15  fun prove_case_equation (arg,con_def) =
    1.16 -    prove_term (sign_of thy) [] 
    1.17 -        (mk_case_equation arg, case_tacsf con_def);
    1.18 +    prove_goalw_cterm [] 
    1.19 +        (cterm_of (sign_of thy) (mk_case_equation arg))
    1.20 +	(case_tacsf con_def);
    1.21  
    1.22  val free_iffs = 
    1.23      map standard (con_defs RL [def_swap_iff]) @
     2.1 --- a/src/ZF/ind_syntax.ML	Thu Aug 18 12:56:57 1994 +0200
     2.2 +++ b/src/ZF/ind_syntax.ML	Thu Aug 18 17:41:40 1994 +0200
     2.3 @@ -14,28 +14,12 @@
     2.4  (*Make a definition lhs==rhs, checking that vars on lhs contain those of rhs*)
     2.5  fun mk_defpair (lhs, rhs) = 
     2.6    let val Const(name, _) = head_of lhs
     2.7 -      val dummy = assert (term_vars rhs subset term_vars lhs
     2.8 -		          andalso
     2.9 -		          term_frees rhs subset term_frees lhs
    2.10 -		          andalso
    2.11 -		          term_tvars rhs subset term_tvars lhs
    2.12 -		          andalso
    2.13 -		          term_tfrees rhs subset term_tfrees lhs)
    2.14 -	          ("Extra variables on RHS in definition of " ^ name)
    2.15    in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
    2.16  
    2.17  fun get_def thy s = get_axiom thy (s^"_def");
    2.18  
    2.19  fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
    2.20  
    2.21 -(*export to Pure/library?  *)
    2.22 -fun assert_all pred l msg_fn = 
    2.23 -  let fun asl [] = ()
    2.24 -	| asl (x::xs) = if pred x then asl xs
    2.25 -	                else error (msg_fn x)
    2.26 -  in  asl l  end;
    2.27 -
    2.28 -
    2.29  (** Abstract syntax definitions for FOL and ZF **)
    2.30  
    2.31  val iT = Type("i",[])
    2.32 @@ -78,15 +62,6 @@
    2.33  val Trueprop = Const("Trueprop",oT-->propT);
    2.34  fun mk_tprop P = Trueprop $ P;
    2.35  
    2.36 -(*Prove a goal stated as a term, with exception handling*)
    2.37 -fun prove_term sign defs (P,tacsf) = 
    2.38 -    let val ct = cterm_of sign P
    2.39 -    in  prove_goalw_cterm defs ct tacsf
    2.40 -	handle e => (writeln ("Exception in proof of\n" ^
    2.41 -			       string_of_cterm ct); 
    2.42 -		     raise e)
    2.43 -    end;
    2.44 -
    2.45  (*Read an assumption in the given theory*)
    2.46  fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
    2.47  
    2.48 @@ -127,21 +102,6 @@
    2.49    | chk_prem rec_hd t = 
    2.50  	deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
    2.51  
    2.52 -
    2.53 -(*Inverse of varifyT.  Move to Pure/type.ML?*)
    2.54 -fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
    2.55 -  | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
    2.56 -  | unvarifyT T = T;
    2.57 -
    2.58 -(*Inverse of varify.  Move to Pure/logic.ML?*)
    2.59 -fun unvarify (Const(a,T))    = Const(a, unvarifyT T)
    2.60 -  | unvarify (Var((a,0), T)) = Free(a, unvarifyT T)
    2.61 -  | unvarify (Var(ixn,T))    = Var(ixn, unvarifyT T)	(*non-zero index!*)
    2.62 -  | unvarify (Abs (a,T,body)) = Abs (a, unvarifyT T, unvarify body)
    2.63 -  | unvarify (f$t) = unvarify f $ unvarify t
    2.64 -  | unvarify t = t;
    2.65 -
    2.66 -
    2.67  (*Make distinct individual variables a1, a2, a3, ..., an. *)
    2.68  fun mk_frees a [] = []
    2.69    | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
     3.1 --- a/src/ZF/indrule.ML	Thu Aug 18 12:56:57 1994 +0200
     3.2 +++ b/src/ZF/indrule.ML	Thu Aug 18 17:41:40 1994 +0200
     3.3 @@ -69,9 +69,10 @@
     3.4  val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) intr_tms;
     3.5  
     3.6  val quant_induct = 
     3.7 -    prove_term sign part_rec_defs 
     3.8 -      (list_implies (ind_prems, mk_tprop (mk_all_imp(big_rec_tm,pred))),
     3.9 -       fn prems =>
    3.10 +    prove_goalw_cterm part_rec_defs 
    3.11 +      (cterm_of sign (list_implies (ind_prems, 
    3.12 +				    mk_tprop (mk_all_imp(big_rec_tm,pred)))))
    3.13 +      (fn prems =>
    3.14         [rtac (impI RS allI) 1,
    3.15  	etac raw_induct 1,
    3.16  	REPEAT (FIRSTGOAL (eresolve_tac [CollectE,exE,conjE,disjE,ssubst])),
    3.17 @@ -118,9 +119,9 @@
    3.18  and mutual_induct_concl = mk_tprop(fold_bal (app conj) qconcls);
    3.19  
    3.20  val lemma = (*makes the link between the two induction rules*)
    3.21 -    prove_term sign part_rec_defs 
    3.22 -	  (mk_implies (induct_concl,mutual_induct_concl), 
    3.23 -	   fn prems =>
    3.24 +    prove_goalw_cterm part_rec_defs 
    3.25 +	  (cterm_of sign (mk_implies (induct_concl,mutual_induct_concl)))
    3.26 +	  (fn prems =>
    3.27  	   [cut_facts_tac prems 1,
    3.28  	    REPEAT (eresolve_tac [asm_rl,conjE,PartE,mp] 1
    3.29  	     ORELSE resolve_tac [allI,impI,conjI,Part_eqI] 1
    3.30 @@ -145,10 +146,11 @@
    3.31  	i  THEN mutual_ind_tac prems (i-1);
    3.32  
    3.33  val mutual_induct_fsplit = 
    3.34 -    prove_term sign []
    3.35 -	  (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,
    3.36 -			 mutual_induct_concl),
    3.37 -	   fn prems =>
    3.38 +    prove_goalw_cterm []
    3.39 +	  (cterm_of sign
    3.40 +	   (list_implies (map (induct_prem (rec_tms~~preds)) intr_tms,
    3.41 +			  mutual_induct_concl)))
    3.42 +	  (fn prems =>
    3.43  	   [rtac (quant_induct RS lemma) 1,
    3.44  	    mutual_ind_tac (rev prems) (length prems)]);
    3.45  
     4.1 --- a/src/ZF/intr_elim.ML	Thu Aug 18 12:56:57 1994 +0200
     4.2 +++ b/src/ZF/intr_elim.ML	Thu Aug 18 17:41:40 1994 +0200
     4.3 @@ -60,11 +60,12 @@
     4.4  val _ = writeln "  Proving monotonicity...";
     4.5  
     4.6  val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) =
     4.7 -    big_rec_def |> rep_thm |> #prop |> unvarify;
     4.8 +    big_rec_def |> rep_thm |> #prop |> Logic.unvarify;
     4.9  
    4.10  val bnd_mono = 
    4.11 -    prove_term sign [] (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs), 
    4.12 -       fn _ =>
    4.13 +    prove_goalw_cterm [] 
    4.14 +      (cterm_of sign (mk_tprop (Fp.bnd_mono $ dom_sum $ fp_abs)))
    4.15 +      (fn _ =>
    4.16         [rtac (Collect_subset RS bnd_monoI) 1,
    4.17  	REPEAT (ares_tac (basic_monos @ monos) 1)]);
    4.18  
    4.19 @@ -102,8 +103,9 @@
    4.20  	and g rl = rl RS disjI2
    4.21      in  accesses_bal(f, g, asm_rl)  end;
    4.22  
    4.23 -val intrs = map (prove_term sign part_rec_defs) 
    4.24 -	       (intr_tms ~~ map intro_tacsf (mk_disj_rls(length intr_tms)));
    4.25 +val intrs = map (uncurry (prove_goalw_cterm part_rec_defs))
    4.26 +            (map (cterm_of sign) intr_tms ~~ 
    4.27 +	     map intro_tacsf (mk_disj_rls(length intr_tms)));
    4.28  
    4.29  (********)
    4.30  val _ = writeln "  Proving the elimination rule...";