1(* Title: ZF/ind_syntax.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1993 University of Cambridge 4 5Abstract Syntax functions for Inductive Definitions. 6*) 7 8structure Ind_Syntax = 9struct 10 11(*Print tracing messages during processing of "inductive" theory sections*) 12val trace = Unsynchronized.ref false; 13 14fun traceIt msg thy t = 15 if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t) 16 else t; 17 18 19(** Abstract syntax definitions for ZF **) 20 21val iT = Type(\<^type_name>\<open>i\<close>, []); 22 23(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *) 24fun mk_all_imp (A,P) = 25 FOLogic.all_const iT $ 26 Abs("v", iT, FOLogic.imp $ (\<^const>\<open>mem\<close> $ Bound 0 $ A) $ 27 Term.betapply(P, Bound 0)); 28 29fun mk_Collect (a, D, t) = \<^const>\<open>Collect\<close> $ D $ absfree (a, iT) t; 30 31(*simple error-checking in the premises of an inductive definition*) 32fun chk_prem rec_hd (Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _) = 33 error"Premises may not be conjuctive" 34 | chk_prem rec_hd (Const (\<^const_name>\<open>mem\<close>, _) $ t $ X) = 35 (Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ()) 36 | chk_prem rec_hd t = 37 (Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ()); 38 39(*Return the conclusion of a rule, of the form t:X*) 40fun rule_concl rl = 41 let val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>mem\<close>, _) $ t $ X) = 42 Logic.strip_imp_concl rl 43 in (t,X) end; 44 45(*As above, but return error message if bad*) 46fun rule_concl_msg sign rl = rule_concl rl 47 handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ 48 Syntax.string_of_term_global sign rl); 49 50(*For deriving cases rules. CollectD2 discards the domain, which is redundant; 51 read_instantiate replaces a propositional variable by a formula variable*) 52val equals_CollectD = 53 Rule_Insts.read_instantiate \<^context> [((("W", 0), Position.none), "Q")] ["Q"] 54 (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2})); 55 56 57(** For datatype definitions **) 58 59(*Constructor name, type, mixfix info; 60 internal name from mixfix, datatype sets, full premises*) 61type constructor_spec = 62 (string * typ * mixfix) * string * term list * term list; 63 64fun dest_mem (Const (\<^const_name>\<open>mem\<close>, _) $ x $ A) = (x, A) 65 | dest_mem _ = error "Constructor specifications must have the form x:A"; 66 67(*read a constructor specification*) 68fun read_construct ctxt (id: string, sprems, syn: mixfix) = 69 let val prems = map (Syntax.parse_term ctxt #> Type.constraint FOLogic.oT) sprems 70 |> Syntax.check_terms ctxt 71 val args = map (#1 o dest_mem) prems 72 val T = (map (#2 o dest_Free) args) ---> iT 73 handle TERM _ => error 74 "Bad variable in constructor specification" 75 in ((id,T,syn), id, args, prems) end; 76 77val read_constructs = map o map o read_construct; 78 79(*convert constructor specifications into introduction rules*) 80fun mk_intr_tms sg (rec_tm, constructs) = 81 let 82 fun mk_intr ((id,T,syn), name, args, prems) = 83 Logic.list_implies 84 (map FOLogic.mk_Trueprop prems, 85 FOLogic.mk_Trueprop 86 (\<^const>\<open>mem\<close> $ list_comb (Const (Sign.full_bname sg name, T), args) 87 $ rec_tm)) 88 in map mk_intr constructs end; 89 90fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg); 91 92fun mk_Un (t1, t2) = \<^const>\<open>Un\<close> $ t1 $ t2; 93 94(*Make a datatype's domain: form the union of its set parameters*) 95fun union_params (rec_tm, cs) = 96 let val (_,args) = strip_comb rec_tm 97 fun is_ind arg = (type_of arg = iT) 98 in case filter is_ind (args @ cs) of 99 [] => \<^const>\<open>zero\<close> 100 | u_args => Balanced_Tree.make mk_Un u_args 101 end; 102 103 104(*Includes rules for succ and Pair since they are common constructions*) 105val elim_rls = 106 [@{thm asm_rl}, @{thm FalseE}, @{thm succ_neq_0}, @{thm sym} RS @{thm succ_neq_0}, 107 @{thm Pair_neq_0}, @{thm sym} RS @{thm Pair_neq_0}, @{thm Pair_inject}, 108 make_elim @{thm succ_inject}, @{thm refl_thin}, @{thm conjE}, @{thm exE}, @{thm disjE}]; 109 110 111(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*) 112fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) 113 | tryres (th, []) = raise THM("tryres", 0, [th]); 114 115fun gen_make_elim elim_rls rl = 116 Drule.export_without_context (tryres (rl, elim_rls @ [revcut_rl])); 117 118(*Turns iff rules into safe elimination rules*) 119fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]); 120 121end; 122 123