TFL/tfl.sml
changeset 6566 7ed743d18af7
parent 6498 1ebbe18fe236
child 7052 4c201f27c74e
equal deleted inserted replaced
6565:de4acf4449fa 6566:7ed743d18af7
   287          else check rst
   287          else check rst
   288  in check (FV_multiset pat)
   288  in check (FV_multiset pat)
   289  end;
   289  end;
   290 
   290 
   291 local fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
   291 local fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
   292       fun single [f] = f
   292       fun single [Free(a,_)] = 
       
   293 	      mk_functional_err (a ^ " has not been declared as a constant")
       
   294         | single [f] = f
   293         | single fs  = mk_functional_err (Int.toString (length fs) ^ 
   295         | single fs  = mk_functional_err (Int.toString (length fs) ^ 
   294                                           " distinct function names!")
   296                                           " distinct function names!")
   295 in
   297 in
   296 fun mk_functional thy clauses =
   298 fun mk_functional thy clauses =
   297  let val (L,R) = ListPair.unzip 
   299  let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses)
   298                     (map (fn (Const("op =",_) $ t $ u) => (t,u)) clauses)
   300                    handle _ => raise TFL_ERR
       
   301 		       {func = "mk_functional", 
       
   302 			mesg = "recursion equations must use the = relation"}
   299      val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
   303      val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
   300      val fcon as Const (fname, ftype) = single (gen_distinct (op aconv) funcs)
   304      val fcon as Const (fname, ftype) = single (gen_distinct (op aconv) funcs)
   301      val dummy = map (no_repeat_vars thy) pats
   305      val dummy = map (no_repeat_vars thy) pats
   302      val rows = ListPair.zip (map (fn x => ([],[x])) pats,
   306      val rows = ListPair.zip (map (fn x => ([],[x])) pats,
   303                               map GIVEN (enumerate R))
   307                               map GIVEN (enumerate R))