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